A Resolution Calculus for First-order Schemata
From MaRDI portal
Publication:2843818
DOI10.3233/FI-2013-855zbMath1319.03033OpenAlexW1765188294MaRDI QIDQ2843818
Vincent Aravantinos, Nicolas Peltier, Mnacho Echenim
Publication date: 26 August 2013
Published in: Fundamenta Informaticae (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.3233/fi-2013-855
Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05)
Related Items (5)
Automated Reasoning Building Blocks ⋮ Cut-Elimination and Proof Schemata ⋮ Schematic refutations of formula schemata ⋮ Combining induction and saturation-based theorem proving ⋮ A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata
This page was built for publication: A Resolution Calculus for First-order Schemata