Automated deduction in classical and non-classical logics : selected papers

Automated Deduction in Classical and Non-Classical Logics: Selected Papers
Author: Ricardo Caferra, Gernot Salzer
Published by Springer Berlin Heidelberg
ISBN: 978-3-540-67190-9
DOI: 10.1007/3-540-46508-1

Table of Contents:

• Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory
• Higher-Order Modal Logic—A Sketch
• Proving Associative-Commutative Termination Using RPO-Compatible Orderings
• Decision Procedures and Model Building or How to Improve Logical Information in Automated Deduction
• Replacement Rules with Definition Detection
• On the Complexity of Finite Sorted Algebras
• A Further and Effective Liberalization of the δ-Rule in Free Variable Semantic Tableaux
• A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set Theory
• Interpretation of a Mizar-Like Logic in First Order Logic
• An
• Implicational Completeness of Signed Resolution
• An Equational Re-engineering of Set Theories
• Issues of Decidability for Description Logics in the Framework of Resolution
• Extending Decidable Clause Classes via Constraints
• Completeness and Redundancy in Constrained Clause Logic
• Effective Properties of Some First Order Intuitionistic Modal Logics
• Hidden Congruent Deduction
• Resolution-Based Theorem Proving for SH
• Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but Without Skolemization

Includes bibliographical references and index