The practicality of generating semantic trees for proofs of unsatisfiability

DOI10.1080/00207169608804524zbMath1001.68513OpenAlexW2079454194MaRDI QIDQ2710799

Monroe M. Newborn, Mohammed Almulla

Publication date: 19 December 2002

Published in: International Journal of Computer Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/00207169608804524

zbMATH Keywords

unsatisfiabilityHerbrand universesemantic treesHerbrand interpretationHerbrand baseHerbrand procedure

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Graph theory (including graph drawing) in computer science (68R10) Semantics in the theory of computing (68Q55)

Related Items

Exploiting parallelism: highly competitive semantic tree theorem prover ⋮ Improving the time efficiency of proving theorems using a learning mechanism

Uses Software

• SETHEO
• TGTP

Cites Work

• Splitting and reduction heuristics in automatic theorem proving
• Experiments with a heuristic theorem-proving program for predicate calculus with equality
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item