Problem solving by searching for models with a theorem prover

DOI10.1016/0004-3702(94)90082-5MaRDI QIDQ1337680zbMATH OpenOpenAlexFDO

Authors Shie-Jue Lee, David A. 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)

Cites work

• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• A structure-preserving clause form translation
• Complete problems in the first-order predicate calculus
• Complexity results for classes of quantificational formulas
• Consistency in networks of relations
• Eliminating dublication with the hyper-linking strategy
• scientific article; zbMATH DE number 4155933 (Why is no real title available?)
• scientific article; zbMATH DE number 4162321 (Why is no real title available?)
• scientific article; zbMATH DE number 3978351 (Why is no real title available?)
• scientific article; zbMATH DE number 4053069 (Why is no real title available?)
• scientific article; zbMATH DE number 4104410 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3774914 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 1995157 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Network-based heuristics for constraint-satisfaction problems
• Non-Horn clause logic programming without contrapositives
• On the complexity of regular resolution and the Davis-Putnam procedure
• Problem corner: Non-Horn problems
• Synthesizing constraint expressions
• The complexity of theorem-proving procedures
• Theorem-Proving on the Computer

Cited in

(1)

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

Describes a project that uses

Uses Software

• OTTER

This page was built for publication: Problem solving by searching for models with a theorem prover

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