An Implementation of the Model Elimination Proof Procedure
From MaRDI portal
Recommendations
- Optimizing proof search in model elimination
- scientific article; zbMATH DE number 1330425
- scientific article; zbMATH DE number 517000
- Publication:4934523
- Model elimination without contrapositives
- The use of lemmas in the model elimination procedure
- scientific article; zbMATH DE number 1696761
- A sequent-style model elimination strategy and a positive refinement
- scientific article; zbMATH DE number 408808
- A proof theory for model checking
Cited in
(20)- Hierarchical deduction
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Refutation graphs
- Analytic resolution in theorem proving
- The use of lemmas in the model elimination procedure
- A disjunctive positive refinement of model elimination and its application to subsumption deletion
- Computing answers with model elimination
- Near-Horn Prolog and the ancestry family of procedures
- Resolution remains hard under equivalence
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- A sequent-style model elimination strategy and a positive refinement
- On the convergence of reduction-based and model-based methods in proof theory
- scientific article; zbMATH DE number 1330425 (Why is no real title available?)
- Subgoal alternation in model elimination
- Optimizing proof search in model elimination
- Loop Elimination, a Sound Optimisation Technique for PTTP Related Theorem Proving
- scientific article; zbMATH DE number 1390242 (Why is no real title available?)
- Seventy Years of Computer Science
- ILF-SETHEO
This page was built for publication: An Implementation of the Model Elimination Proof Procedure
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4770008)
