Original title: External sources of axioms in lean theorem proving
Translated title: External sources of axioms in lean theorem proving
Authors: Brunetto, Robert ; Suda, Martin (advisor) ; Pudlák, Petr (referee)
Document type: Master’s theses
Year: 2012
Language: cze
Abstract: [cze] [eng]
Automatické dokazovače vět lze upravit tak, aby mohly používat externí zdroje axiomů. To bylo nedávno zkoumáno v kombinaci se saturačním dokazovačem SPASS-XDB, který během saturační smyčky odesílá dotazy o externí axiomy a přijímá odpovědi. Lean dokazovače používají sémantický tableau kalkulus. Proto je potřeba pro ně použít jiný přístup. Tato práce představuje myšlenku, že by bylo možné od sebe oddělit dokazování a komunikaci s externími zdroji axiomů a to tak, že se nejprve vygeneruje schématický důkaz, u kterého se až následně kontroluje zda mu odpovídají nějaká externí data a zda ho lze doplnit na důkaz. Součástí této práce je upravená verze dokazovače LeanCoP tak, aby demonstrovala tuto myšlenku a zároveň se ukazuje, že je tento program často efektivnější než SPASS-XDB - dokonce ho poráží i na všech vzorových příkladech z jeho webové stránky. Automated theorem provers can be modified in order to use external sources of axioms. This was recently searched in combination with saturation based theorem prover SPASS-XDB. It sends queries to external sources and receives answers during its saturation loop. Lean theorem provers are based on semantic tableau calculus. That's why they need to use different approach. An idea that proving is separated from communication is beeing introduced by this work. Prover generetes so called schematic proof which is later checked if it can be filled with external data so the proof can be completed. This work demonstates this idea on modified version of LeanCoP.
Keywords: automated theorem proving; external sources of axioms; LeanCoP; LeanCoP-XDB; automatické dokazování vět; externí zdroje axiomů; LeanCoP; LeanCoP-XDB

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/40753

Permalink: http://www.nusl.cz/ntk/nusl-305056


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Master’s theses