A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata

DOI10.1007/978-3-319-08434-3_6zbMath1304.03044OpenAlexW71573974MaRDI QIDQ5495914

David M. Cerna

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08434-3_6

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05)

Uses Software

• CERES

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• The number of proof lines and the size of proofs in first order logic
• Note on the generalization of calculations
• Proof schemata in Hilbert-type axiomatic theories
• A Resolution Calculus for First-order Schemata
• Decidability and Undecidability Results for Propositional Schemata
• Schemata: The Concept of Schema in the History of Logic
• A Schemata Calculus for Propositional Logic
• Some Results on the Length of Proofs
• A Decidable Class of Nested Iterated Schemata

This page was built for publication: A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata