Shota Rustaveli National Science Foundation of GeorgiaStart Date: 2013-12-24 End Date: 2014-12-24
Automated reasoning is one of the most important research area in logic and computer science. It is also considered as a sub-field of artificial intelligence. It studies different aspects of reasoning. The most important tools of automated reasoning are different calculi for classical logic.
There is a lot of work done in automated theorem proving, a subfield of automated reasoning, but many important problems are still remaining. One of them is abuse of a good graphical user interface for theorem provers. All existing theorem provers are not user friendly in a sense that they provide command line interface and bunch of so called flags, which user can manipulate. Nowadays it is actual problem to develop Graphical User Interfaces for theorem provers and there is even workshops addressing this problem.
Automated theorem proving appeared not to be enough to handle interesting proofs, e.g. containing induction. The problem is that the induction rule cannot be expressed in the first-order logic. It is a meta rule, or a rule schema and corresponds to infinitary modus ponens rule. Therefore to handle induction during proof search, provers need human interaction.
Recently there was developed an alternative formalism to inductive systems, called proof schemata, which avoids the use of induction axiom. These schemata are based on primitive-recursive definitions. Formulas and proofs are built in a standard way and then by primitive recursion on them formula- and proof schemata are obtained.
The theorem proving techniques are divided into two parts, goal-directed and refutational. In this project we study a goal-directed proof-search algorithm, which is based on a sequent calculus. Usually sequent calculus inference rules can be applied freely, producing a redundant search space. The technique, called focusing, removes this nondeterminism and redundancy in proof-search. Under the given project we study similar techniques for constructing proof schemata and implement corresponding algorithms.