A Resolution Calculus for First-order Schemata

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

zbMATH Keywords

first-order logicpropositional logicresolution calculusschemataclausal logic

Mathematics Subject Classification ID

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