This volume presents a collection of thoroughly reviewed revised full papers on automated deduction in classical, modal, and many-valued logics, with an emphasis on first-order theories.
Five invited papers by prominent researchers give a consolidated view of the recent developments in first-order theorem proving. The 14 research papers presented went through a twofold selection process and were first presented at the International Workshop on First-Order Theorem Proving, FTP'98, held in Vienna, Austria, in November 1998. The contributed papers reflect the current status in research in the area; most of the results presented rely on resolution or tableaux methods, with a few exceptions choosing the equational paradigm.
Author(s): Gilles Dowek (auth.), Ricardo Caferra, Gernot Salzer (eds.)
Series: Lecture Notes in Computer Science 1761 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2000
Language: English
Pages: 304
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Logics and Meanings of Programs
Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory....Pages 1-22
Higher-Order Modal Logic—A Sketch....Pages 23-38
Proving Associative-Commutative Termination Using RPO-Compatible Orderings....Pages 39-61
Decision Procedures and Model Building or How to Improve Logical Information in Automated Deduction....Pages 62-79
Replacement Rules with Definition Detection....Pages 80-94
On the Complexity of Finite Sorted Algebras....Pages 95-108
A Further and Effective Liberalization of the δ -Rule in Free Variable Semantic Tableaux....Pages 109-125
A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set Theory....Pages 126-136
Interpretation of a Mizar-Like Logic in First Order Logic....Pages 137-151
An $$ \mathcal{O} $$ (( n · log n ) 3 )-Time Transformation from Grz into Decidable Fragments of Classical First-Order Logic....Pages 152-166
Implicational Completeness of Signed Resolution....Pages 167-174
An Equational Re-engineering of Set Theories....Pages 175-190
Issues of Decidability for Description Logics in the Framework of Resolution....Pages 191-205
Extending Decidable Clause Classes via Constraints....Pages 206-220
Completeness and Redundancy in Constrained Clause Logic....Pages 221-235
Effective Properties of Some First Order Intuitionistic Modal Logics....Pages 236-250
Hidden Congruent Deduction....Pages 251-266
Resolution-Based Theorem Proving for SH n -Logics....Pages 267-281
Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ -Rule but Without Skolemization....Pages 282-297
