Unification in sort theories and its applications

DOI10.1007/BF02127750zbMath0887.03006MaRDI QIDQ1380412

Christoph Weidenbach

Publication date: 17 May 1998

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

complexityalgorithmunificationresolutiontableaumany-sorted logicsort theories

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Related Items (5)

Reasoning without believing: on the mechanisation of presuppositions and partiality ⋮ Unification in pseudo-linear sort theories is decidable ⋮ Order-sorted Equational Unification Revisited ⋮ Regular expression order-sorted unification and matching ⋮ Rasiowa-Sikorski deduction systems in computer science applications.

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Order-sorted unification
• Investigations in many-sorted quantor logic
• Termination of rewriting
• A more expressive formulation of many sorted logic
• Unification theory
• The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
• Semantics of order-sorted specifications
• An order-sorted logic for knowledge representation systems
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Linear unification
• Computational aspects of an order-sorted logic with term declarations
• Problem corner: The Lion and the Unicorn
• An improved proof procedure1
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• An Efficient Unification Algorithm
• A Machine-Oriented Logic Based on the Resolution Principle
• A variant of a recursively unsolvable problem

This page was built for publication: Unification in sort theories and its applications