A simplified problem reduction format

DOI10.1016/0004-3702(82)90041-8zbMath0497.68058OpenAlexW2046511504WikidataQ29305654 ScholiaQ29305654MaRDI QIDQ1170894

David Alan Plaisted

Publication date: 1982

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(82)90041-8

zbMATH Keywords

PROLOGnatural deductionplanningresolutionprogram verificationquestion answeringsearch strategiesnon-resolution

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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, Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures, History and Prospects for First-Order Automated 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, Automatic theorem proving. II, The search efficiency of theorem proving strategies, Term rewriting: Some experimental results, Renaming a set of non-Horn clauses, Refutational theorem proving using term-rewriting systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theorem proving with abstraction
• Non-resolution theorem proving
• Untersuchungen über das logische Schliessen. I
• Splitting and reduction heuristics in automatic theorem proving
• Linear resolution with selection function
• Worst Case Exponential Lower Bounds for Input Resolution with Paramodulation
• Unit Refutations and Horn Sets
• A Semantically Guided Deductive System for Automatic Theorem Proving
• A Human Oriented Logic for Automatic Theorem-Proving
• Proving Theorems with the Modification Method
• A Machine-Oriented Logic Based on the Resolution Principle