On Skolemization in constrained logics

DOI10.1007/BF02127744zbMath0887.03005MaRDI QIDQ1380406

Bernhard Hollunder, Armin Laux, Hans-Jürgen Bürckert

Publication date: 17 May 1998

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

zbMATH Keywords

first-order logicsatisfiabilitySkolemizationrestricted quantifiersconstrained logicsconstrained resolution principle

Mathematics Subject Classification ID

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

Related Items (1)

Automatic synthesis of logical models for order-sorted first-order theories

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Investigations in many-sorted quantor logic
• An algebraic semantics approach to the effective resolution of type equations
• The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
• An order-sorted logic for knowledge representation systems
• A resolution principle for constrained logics
• Computational aspects of an order-sorted logic with term declarations
• Automated deduction by theory resolution
• Die Zulässigkeit der Behandlung mehrsortiger Theorien mittels der üblichen einsortigen Prädikatenlogik
• Login: a logic programming language with built-in inheritance
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: On Skolemization in constrained logics