Resolution is cut-free

DOI10.1007/S10817-009-9153-6MaRDI QIDQ972424zbMATH OpenOpenAlexFDO

Authors Olivier Hermant

Publication date 26 May 2010

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-009-9153-6

zbMATH Keywords

resolutionrewritingcut ruleSkolemizationdeduction modulocut-freeclassical sequent calculusENARSkolem theorem

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Theorem proving modulo
• Clausal presentation of theories in deduction modulo
• Cut Elimination in Deduction Modulo by Abstract Completion
• Cut rule for the resolution method
• Cut Admissibility by Saturation

Cites work

• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 15881 (Why is no real title available?)
• scientific article; zbMATH DE number 1088191 (Why is no real title available?)
• scientific article; zbMATH DE number 2079034 (Why is no real title available?)
• scientific article; zbMATH DE number 1765670 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 789391 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3296224 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3074068 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Semantic Completeness Proof for TaMeD
• Automated Reasoning
• Computing small clause normal forms
• Constructivism in mathematics. An introduction. Volume I
• Cut Elimination in Deduction Modulo by Abstract Completion
• Focusing and Polarization in Intuitionistic Logic
• HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
• Handbook of automated reasoning. In 2 vols
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• On Constructive Cut Admissibility in Deduction Modulo
• Proof normalization modulo
• Proof theory. 2nd ed
• Resolution in type theory
• Term Rewriting and Applications
• The inverse method
• The predicate calculus with -symbol
• Theorem proving modulo
• Typed Lambda Calculi and Applications
• Untersuchungen über das logische Schliessen. I
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

Cited in

(7)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Translation of resolution proofs into short first-order proofs without choice axioms.
• Clausal presentation of theories in deduction modulo
• Complexity of translations from resolution to sequent calculus
• Translation of resolution proofs into short first-order proofs without choice axioms
• Linking focusing and resolution with selection
• Linking focusing and resolution with selection

Describes a project that uses

Uses Software

• Zenon
• VAMPIRE

This page was built for publication: Resolution is cut-free

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