Lemma and cut strategies for propositional model elimination

DOI10.1023/A:1018950727018zbMATH Open0940.68119OpenAlexW1573983406MaRDI QIDQ1978019FDOQ1978019

Authors Fumiaki Okushi, Allen Van Gelder 

Publication date 7 June 2000

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1018950727018

zbMATH Keywords

model eliminationmodoc

Mathematics Subject Classification ID

Recommendations

• Persistent and quasi-persistent lemmas in propositional model elimination
• Cut-elimination and proof schemata
• A note on cut-elimination for classical propositional logic
• Cut Elimination and Decidability for Classical Lambek Logic
• Bounds for cut elimination in intuitionistic propositional logic
• scientific article; zbMATH DE number 48659
• The use of lemmas in the model elimination procedure
• Cut elimination for shallow modal logics
• Cut Elimination in the Presence of Axioms
• A cut-elimination proof in intuitionistic predicate logic

Cited in

(5)

• Model elimination without contrapositives
• Persistent and quasi-persistent lemmas in propositional model elimination
• Optimizing proof search in model elimination
• Combining preorder and postorder resolution in a satisfiability solver
• Complexity analysis of propositional resolution with autarky pruning

Describes a project that uses

Uses Software

• SATO
• DIMACS

This page was built for publication: Lemma and cut strategies for propositional model elimination

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