A Simplified Format for the Model Elimination Theorem-Proving Procedure
From MaRDI portal
Publication:5574714
DOI10.1145/321526.321527zbMath0183.29603OpenAlexW2042551813MaRDI QIDQ5574714
Publication date: 1969
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321526.321527
Related Items
TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic, Semantically-guided goal-sensitive reasoning: model representation, 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, History and Prospects for First-Order Automated Deduction, Hierarchical deduction, A Prolog technology theorem prover: Implementation by an extended Prolog compiler, Near-Horn Prolog and the ancestry family of procedures, Non-Horn clause logic programming, Subsumption-linear Q-resolution for QBF theorem proving, Complexity analysis of propositional resolution with autarky pruning, Connection tableaux with lazy paramodulation, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, Another look at graph coloring via propositional satisfiability, Incremental theory reasoning methods for semantic tableaux, A semantic backward chaining proof system, Linear resolution for consequence finding, A Prolog technology theorem prover: A new exposition and implementation in Prolog, Controlled use of clausal lemmas in connection tableau calculi, John McCarthy's legacy, Refutation graphs, Building Theorem Provers, The search efficiency of theorem proving strategies, On the relation between resolution based and completion based theorem proving, Linear resolution with selection function, Lemma matching for a PTTP-based top-down theorem prover, The linked conjunct method for automatic deduction and related search techniques, Renaming a set of non-Horn clauses, Set of support, demodulation, paramodulation: a historical perspective
