Lecturers: Alexander Leitsch, Bernhard Gramlich
Description of the course in TISS: Here.
The project is an obligatory part of the International Master Study Computational Logic.
Contents / Possible Projects:
Programming and Experiments with the System CERES
CERES (= cut-elimination by resolution) is a system for automated proof transformation, in particular for cut-elimination in real mathematical proofs. The core of the cut-elimination procedure is a clausal theorem prover; this prover is used to refute the so-called characteristic clause set which contains the essence of the original proof. The resolution refutation obtained by the prover represents the skeleton of a cut-free proof and contains the key for constructions and algorithms corresponding to the new cut-free proof. As the characteristic clause sets typically contain complex mathematical information, current theorem provers frequently fail to refute the set. Therefore it is desirable to develop more efficient theorem proving methods for the needs of CERES
The purpose of this project is the further development of the theorem proving environment of CERES; this includes the development and programming of specific algorithms and heuristics, the comparison of different theorem provers, and their evaluation w.r.t. CERES.
Programming and Experiments with the System VMTL
VMTL (Vienna Modular Termination Laboratory) is a tool for the (semi-)automatic termination analysis of various types of (first-order) term rewriting systems. Currently, standard as well as context-sensitive and conditional term rewriting systems are supported.
VMTL is based on the dependency pair framework, in which termination of rewrite systems is analyzed by so-called dependency pair processors. The search for termination proofs in VMTL is guided by a user configurable strategy featuring hierarchical grouping of processors, time-limits on the level of processor groups as well as single processors and parallelization. In addition VMTL provides open interfaces allowing to add new dependency pair processors as well as transformations/preprocessings of rewrite systems in a modular fashion. Two user front-ends are available, a web application and a command line interface.
Possible topics for the Project in Computational Logic in the context of VMTL include extending its functionality by specific features / termination proof methods (which requires good programming skills in Java) and and/or performing systematic extensive experiments with the system relying in particular on the TPDP (Termination Problem Data Base). Both types of tasks assume or require, respectively, at least some basic knowledge in term rewriting.
Contact / Registration
A.Leitsch,
B.Gramlich