Automated Deduction in Classical and Non-Classical Logics: Selected PapersAuthor: Ricardo Caferra, Gernot Salzer Published by Springer Berlin Heidelberg ISBN: 978-3-540-67190-9 DOI: 10.1007/3-540-46508-1Table 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