Skip to main content
To KTH's start page

Gustav Yilbar Kjellström: Kvantifikatorelimination

BSc Thesis Presentation

Time: Tue 2020-09-01 14.00 - 15.00

Location: Zoom, meeting ID: 8678769725

Participating: Gustav Yilbar Kjellström

Supervisor: Torbjörn Tambour

Export to calendar

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.