Problem solving by searching for models with a theorem prover

DOI10.1016/0004-3702(94)90082-5zbMath0941.68740OpenAlexW2047274827MaRDI QIDQ1337680

Shie-Jue Lee, David Alan Plaisted

Publication date: 26 February 1996

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

Full work available at URL: https://doi.org/10.1016/0004-3702(94)90082-5

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures

Uses Software

• OTTER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Eliminating dublication with the hyper-linking strategy
• Complete problems in the first-order predicate calculus
• A structure-preserving clause form translation
• Network-based heuristics for constraint-satisfaction problems
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Non-Horn clause logic programming without contrapositives
• Complexity results for classes of quantificational formulas
• Consistency in networks of relations
• On the complexity of regular resolution and the Davis-Putnam procedure
• Problem corner: Non-Horn problems
• Theorem-Proving on the Computer
• Synthesizing constraint expressions
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• The complexity of theorem-proving procedures