The Relative Power of Semantics and Unification

DOI10.1007/978-3-642-37651-1_14zbMath1383.68081OpenAlexW148444778MaRDI QIDQ4916085

Swaha Miller, David Alan Plaisted

Publication date: 19 April 2013

Published in: Programming Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-37651-1_14

zbMATH Keywords

theorem provingunificationsemanticspropositional calculusOSHL

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (2)

Semantically-guided goal-sensitive reasoning: model representation ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness

Uses Software

• OTTER
• VAMPIRE
• TPTP
• DCTP
• iProver-Eq
• iProver
• UCPOP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Eliminating dublication with the hyper-linking strategy
• The TPTP problem library. CNF release v1. 2. 1
• Ordered semantic hyper-linking
• Automated deduction by theory resolution
• Ordered semantic hyper tableaux
• The model evolution calculus as a first-order DPLL method
• STRIPS: A new approach to the application of theorem proving to problem solving
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• ADL and the State-Transition Model of Action
• Model Evolution with Equality Modulo Built-in Theories
• Computer Science Logic
• Automated Deduction – CADE-20
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Automated Deduction – CADE-19

This page was built for publication: The Relative Power of Semantics and Unification