Thesis (Selection of subject)Thesis (Selection of subject)(version: 368)
Thesis details
   Login via CAS
External sources of axioms in lean theorem proving
Thesis title in Czech: External sources of axioms in lean theorem proving
Thesis title in English: External sources of axioms in lean theorem proving
Key words: automatické dokazování vět, externí zdroje axiomů, LeanCoP, LeanCoP-XDB
English key words: automated theorem proving, external sources of axioms, LeanCoP, LeanCoP-XDB
Academic year of topic announcement: 2011/2012
Thesis type: diploma thesis
Thesis language: čeština
Department: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Supervisor: RNDr. Martin Suda, Ph.D.
Author: hidden - assigned and confirmed by the Study Dept.
Date of registration: 12.05.2011
Date of assignment: 12.05.2011
Confirmed by Study dept. on: 01.08.2012
Date and time of defence: 03.09.2012 09:00
Date of electronic submission:01.08.2012
Date of submission of printed version:01.08.2012
Date of proceeded defence: 03.09.2012
Opponents: RNDr. Petr Pudlák, Ph.D.
 
 
 
Advisors: RNDr. Martin Suda, Ph.D.
Guidelines
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.
References
[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).
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html