We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Proof compressions with circuit-structured substitutions.
- Authors
Gordeev, L.; Haeusler, E. H.; da Costa, V. G.
- Abstract
It is well known that the size of propositional classical proofs can be huge. Proof-theoretical studies discovered exponential gaps between cut-free (or normal) proofs and the corresponding (non-normal) proofs with cuts (or modus ponens). The task of automatic theorem proving is, on the other hand, usually based on the construction of cut-free or only atomic-cuts proofs, since this procedure produces less alternative choices. There are familiar tautologies whose cut-free proofs are huge while the non-cut-free ones are small. The aim of this paper is to discuss basic methods of weight and/or size reduction of deductions by switching from traditional tree-structured deductions to circuit-structured deductions. A desired efficiency is achieved by adding the standard weakening rule of inference upgraded by adding suitable (propositional) unifications modulo variable substitutions. We show examples where such a unification provides strong (in fact, exponential) compression of cut-free deductions. Bibliography: 10 titles.
- Subjects
PROOF theory; AUTOMATIC theorem proving; PROPOSITIONAL calculus; EXPONENTIAL functions; NORMAL numbers
- Publication
Journal of Mathematical Sciences, 2009, Vol 158, Issue 5, p645
- ISSN
1072-3374
- Publication type
Article
- DOI
10.1007/s10958-009-9405-3