Non-Horn clause logic programming without contrapositives
From MaRDI portal
Publication:1116717
DOI10.1007/BF00244944zbMath0666.68091OpenAlexW1998330152MaRDI QIDQ1116717
Publication date: 1988
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00244944
Related Items
Conditional term rewriting and first-order theorem proving, TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic, Problem solving by searching for models with a theorem prover, Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction, History and Prospects for First-Order Automated Deduction, A Prolog technology theorem prover: Implementation by an extended Prolog compiler, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, Near-Horn Prolog and the ancestry family of procedures, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Non-Horn clause logic programming, Computing answers with model elimination, A semantic backward chaining proof system, A Prolog technology theorem prover: A new exposition and implementation in Prolog, Refinements to depth-first iterative-deepening search in automatic theorem proving, The search efficiency of theorem proving strategies, Model elimination without contrapositives, Semantically guided first-order theorem proving using hyper-linking, The TPTP problem library, Term rewriting: Some experimental results, Lemma matching for a PTTP-based top-down theorem prover, Renaming a set of non-Horn clauses, A typed resolution principle for deduction with conditional typing theory
