The Relative Power of Semantics and Unification

DOI10.1007/978-3-642-37651-1_14MaRDI QIDQ4916085zbMATH OpenOpenAlexFDO

Authors Swaha Miller, David A. 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

semanticstheorem provingunificationpropositional calculusOSHL

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• On the semantics of unification grammars
• Semantic unification. A sheaf theoretic approach to natural language
• The semantical hyperunification problem
• scientific article; zbMATH DE number 2186289
• scientific article; zbMATH DE number 4031035
• scientific article; zbMATH DE number 2059537
• The logic of unification in grammar
• Inconsistency and semantic unification
• scientific article; zbMATH DE number 3966049

Cites work

• scientific article; zbMATH DE number 1614697 (Why is no real title available?)
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 1765683 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A machine program for theorem-proving
• ADL and the State-Transition Model of Action
• Automated Deduction – CADE-20
• Automated deduction by theory resolution
• Computer Science Logic
• Eliminating dublication with the hyper-linking strategy
• Model Evolution with Equality Modulo Built-in Theories
• Ordered semantic hyper tableaux
• Ordered semantic hyper-linking
• 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
• The TPTP problem library. CNF release v1. 2. 1
• The model evolution calculus as a first-order DPLL method
• The model evolution calculus.
• The state of CASC
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality

Cited in

(5)

• scientific article; zbMATH DE number 1954191 (Why is no real title available?)
• Inconsistency and semantic unification
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Semantically-guided goal-sensitive reasoning: model representation
• Automated Reasoning with Analytic Tableaux and Related Methods

Describes a project that uses

Uses Software

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

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

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