Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 368)
Detail práce
   Přihlásit přes CAS
External sources of axioms in lean theorem proving
Název práce v češtině: External sources of axioms in lean theorem proving
Název v anglickém jazyce: External sources of axioms in lean theorem proving
Klíčová slova: automatické dokazování vět, externí zdroje axiomů, LeanCoP, LeanCoP-XDB
Klíčová slova anglicky: automated theorem proving, external sources of axioms, LeanCoP, LeanCoP-XDB
Akademický rok vypsání: 2011/2012
Typ práce: diplomová práce
Jazyk práce: čeština
Ústav: Katedra teoretické informatiky a matematické logiky (32-KTIML)
Vedoucí / školitel: RNDr. Martin Suda, Ph.D.
Řešitel: skrytý - zadáno a potvrzeno stud. odd.
Datum přihlášení: 12.05.2011
Datum zadání: 12.05.2011
Datum potvrzení stud. oddělením: 01.08.2012
Datum a čas obhajoby: 03.09.2012 09:00
Datum odevzdání elektronické podoby:01.08.2012
Datum odevzdání tištěné podoby:01.08.2012
Datum proběhlé obhajoby: 03.09.2012
Oponenti: RNDr. Petr Pudlák, Ph.D.
 
 
 
Konzultanti: RNDr. Martin Suda, Ph.D.
Zásady pro vypracování
The thesis explores how a lean theorem prover (such as LeanCoP [1], or
LeanTAP [2]) can be adapted to obtain axioms from external sources.
The idea of connecting an automated theorem prover to external sources
of axioms has recently been studied in the context of saturation
theorem prover [3]. Lean theorem provers (typically programmed in
Prolog) are based on completely different approach of semantic
tableaux [4], which requires novel ideas to be developed to realize
similar integration. The external sources from [3] are freely
available, and thus a direct comparison of the two paradigms should be
one of the thesis' outputs. Other possible direction is theorem
proving in arithmetical theories with the help of computed axioms
coming from a computer algebra system.
Seznam odborné literatury
[1] J. Otten, W. Bibel: LeanCoP: Lean Connection-Based Theorem
Proving, in Journal of Symbolic Computation, Volume 36, pages 139-161.
Elsevier Science (2003).

[2] B. Beckert, J. Posegga: LeanTAP: Lean, Tableau-based Deduction, in
Journal of Automated Reasoning, Vol. 15, No. 3, pages 339-358, (1995).

[3] M. Suda, G. Sutcliffe, P. Wischnewski, M. Lamotte-Schubert, G. de
Melo: External Sources of Axioms in Automated Theorem Proving, in
Proceedings of the 32nd Annual Conference on Artificial Intelligence
(eds. B. Mertsching), LNAI 5803, pp. 281-288. Springer, Heidelberg
(2009).

[4] M. Fitting: First-Order Logic and Automated Theorem Proving (2nd
ed.). Springer (1996).
 
Univerzita Karlova | Informační systém UK