A Simplified Format for the Model Elimination Theorem-Proving Procedure

Cited in

(30)

Hierarchical deduction
A Prolog technology theorem prover: Implementation by an extended Prolog compiler
A semantic backward chaining proof system
Linear resolution for consequence finding
A Prolog technology theorem prover: A new exposition and implementation in Prolog
Refutation graphs
TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic
Controlled integration of the cut rule into connection tableau calculi
Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
Non-Horn clause logic programming
Renaming a set of non-Horn clauses
The linked conjunct method for automatic deduction and related search techniques
Near-Horn Prolog and the ancestry family of procedures
Complexity analysis of propositional resolution with autarky pruning
Set of support, demodulation, paramodulation: a historical perspective
Towards a unified model of search in theorem-proving: subgoal-reduction strategies
Another look at graph coloring via propositional satisfiability
Linear resolution with selection function
Semantically-guided goal-sensitive reasoning: model representation
History and prospects for first-order automated deduction
Incremental theory reasoning methods for semantic tableaux
Building Theorem Provers
The search efficiency of theorem proving strategies
Lemma matching for a PTTP-based top-down theorem prover
John McCarthy's legacy
Controlled use of clausal lemmas in connection tableau calculi
Subsumption-linear Q-resolution for QBF theorem proving
A complete semantic back chaining proof system
On the relation between resolution based and completion based theorem proving
Connection tableaux with lazy paramodulation

This page was built for publication: A Simplified Format for the Model Elimination Theorem-Proving Procedure

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