Proof schemata in Hilbert-type axiomatic theories

DOI10.1007/BF01098278MaRDI QIDQ2276941zbMATH OpenOpenAlexFDO

Authors V. P. Orevkov

Publication date 1991

Published in Journal of Soviet Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01098278

zbMATH Keywords

Hilbert-type theoriesproof schemes

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Complexity of proofs (03F20)

Review text

[For the entire collection see Zbl 0657.00011.] See the review in Zbl 0694.03009.

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• scientific article; zbMATH DE number 4170894 (Why is no real title available?)
• scientific article; zbMATH DE number 4039891 (Why is no real title available?)
• scientific article; zbMATH DE number 3361272 (Why is no real title available?)
• Linear unification
• Some Results on the Length of Proofs
• The number of proof lines and the size of proofs in first order logic

Cited in

(5)

• Bounded arithmetic, proof complexity and two papers of Parikh
• Refinement of bounds of the height of terms in the most general unifier
• Schematic refutations of formula schemata
• A tableaux-based decision procedure for multi-parameter propositional schemata
• A decidable class of nested iterated schemata

This page was built for publication: Proof schemata in Hilbert-type axiomatic theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2276941)