On the calculus of positively constructed formulas for automated theorem proving |
| |
Authors: | A V Davydov A A Larionov E A Cherkashin |
| |
Affiliation: | 1.Institute of Systems Dynamics and Control Theory,SB RAS,Irkutsk,Russia;2.Institute of Mathematics, Economics and Computer Science,Irkutsk State University,Irkutsk,Russia |
| |
Abstract: | The paper deals with an expressive logic language LF and its calculus. Formulas of this language consist of some large-scale structural elements, such as type quantifiers. The
language LF contains only two logic symbols—∀ and ∃, which form the set of logic connectives of the language. The logic calculus JF and complete strategy for automated proof search based on a single unary rule of inference are considered. This calculus
has a number of other features which lead to the reduction of the combinatorial complexity of finding the deductions in comparison
to the known systems for automated theorem proving as the Resolution method and Genzen calculus. Problems of effective implementation
of JF as a program system for automated theorem proving are considered. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|