The practicality of generating semantic trees for proofs of unsatisfiability

DOI10.1080/00207169608804524MaRDI QIDQ2710799zbMATH OpenOpenAlexFDO

Authors M. Almulla, Monroe M. Newborn

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

Herbrand baseHerbrand interpretationHerbrand procedureHerbrand universesemantic treesunsatisfiability

Mathematics Subject Classification ID

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

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Experiments with a heuristic theorem-proving program for predicate calculus with equality
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Splitting and reduction heuristics in automatic theorem proving

Cited in

(2)

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

Describes a project that uses

Uses Software

• SETHEO
• TGTP

This page was built for publication: The practicality of generating semantic trees for proofs of unsatisfiability

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