Gustav Yilbar Kjellström: Kvantifikatorelimination

Abstract

Syftet med detta arbete är att undersöka hur man eliminerar kvantifikatorer med hjälp av en generalisering av Sturms sats, samt undersöka hur Mathematica klarar av att eliminera kvantifikatorer. Detta arbete inkluderar ett bevis av Sturms sats. Denna sats kan man använda för att bestämma antalet reella nollstället till ett polynom, men fokuset ligger på en generalisering av Sturms sats som säger att man kan skriva om ett uttryck till ett ekvivalent kvantifikatorfritt uttryck och därigenom eliminera alla kvantifikatorer. Slutligen undersöks Mathematicas begränsningar samt hur programmet svarar när man använder dess inbygga funktion resolve för att eliminera kvantifikatorer. Detta undersöks på några geometriska former som tex skärning mellan två linjer.