Automated Deduction in Classical and Non-Classical Logics: Selected Papers (Lecture Notes in Computer Science, 1761)

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. Cover......Page 1 Automated Deduction in Classical and Non-Classical Logics, Selected Papers......Page 4 ISBN 3540671900......Page 5 Preface......Page 6 Table of Contents......Page 8 Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory......Page 10 1.1 Deduction Modulo......Page 11 1.2 Resolution Modulo......Page 12 1.3 Cut Elimination and Completeness......Page 14 2.1 Simple Type Theory......Page 15 2.2 Set Theory......Page 16 3.1 Resolution Modulo in Type Theory......Page 18 4.2 Completeness......Page 19 4.4 The Role of Unification and Extended Narrowing......Page 20 5 Advanced Formulations of Type Theory and Set Theory......Page 21 6.1 In Type Theory with a Function......Page 23 6.2 In Type Theory with a Relation......Page 25 6.4 Remarks......Page 27 References......Page 29 1 Introduction......Page 32 2 Syntax......Page 34 3 Models......Page 37 4 Truth......Page 38 5 Non-standard Models......Page 39 6 Tableaus......Page 40 7 Tableau Examples......Page 44 References......Page 47 1 Introduction......Page 48 2 Rewrite Systems and Simplification Orderings......Page 50 2.1 Recursive Path Ordering......Page 51 2.3 Flattening......Page 52 3 Issues in Extending RPO to AC-Terms......Page 53 3.1 Candidates......Page 55 3.2 Context Comparison......Page 57 4 Definition of AC-RPO ( )......Page 58 4.1 Properties of Candidates ......Page 59 4.2 Comparing Terms......Page 60 5 Proofs......Page 62 6 Stability of >ac......Page 65 References......Page 69 1 Introduction......Page 71 2 Notation and Definitions......Page 73 3 Theorem Provers as Decision Procedures......Page 74 4 Extraction of Models......Page 77 5 Extensions of Clause Logic......Page 83 References......Page 87 1 Introduction......Page 89 2 Replacement Rules......Page 90 3 Methods for Choosing Replacement Rules......Page 92 4 Test Results......Page 98 5 Comparison with Other Approaches......Page 99 6 Discussion......Page 100 7 Conclusions......Page 101 References......Page 102 1 Introduction......Page 104 2 Preliminaries......Page 105 3 Non-monadic Signatures......Page 109 4 Hard Monadic Signatures......Page 112 5 Easy Monadic Signatures......Page 114 References......Page 117 1 Introduction......Page 118 2.2 Structures and Assignments......Page 119 2.4 Different Variants of the Delta-Rule......Page 120 3.1 Canonical and Key Formulae......Page 122 3.2 Relevant Extracted Formulae......Page 124 3.3 The -Rule......Page 125 4 Completeness and Soundness of the Delta-Rule......Page 127 5.1 Comparing the Delta-Rule to Other Versions......Page 129 5.2 Exponential Speedup......Page 130 5.3 Non-elementary Speedup......Page 131 6 Conclusions and Directions of Future Research......Page 132 References......Page 134 1 Introduction......Page 135 2.2 Semantics......Page 136 2.3 Realizations......Page 137 3.1 Saturation Rules......Page 138 4 The Decision Procedure......Page 141 4.2 Partial Correctness......Page 142 6 Future Plans......Page 144 References......Page 145 2 Semantic Foundations......Page 146 3 Interpretations......Page 147 4.1 On the Mizar Type System......Page 149 4.2 Semantics of Mizar Types......Page 151 4.3 A Remark on the Power of the Mizar Type System......Page 152 5 Interpretations of Mizar Formulas in First Order Logic......Page 153 6 Modifications......Page 158 7 Discussion......Page 159 References......Page 160 1 Introduction......Page 161 2 Basic Notions......Page 163 3 A Transformation from Grz into S4......Page 165 4 A Transformation from S4 into T......Page 168 References......Page 174 1 Implicational Completeness A Neglected Topic......Page 176 2 Signed Clause Logic......Page 177 3 Signed Resolution......Page 178 4 Implication and Subsumption......Page 179 5 Semantic Trees for Signed Clause Logic......Page 180 6 Implicational Completeness......Page 182 References......Page 183 1 Introduction......Page 184 2 Syntax and Semantics of L......Page 185 3 Specifying Set Theories in L......Page 187 4 Extensionality, Subset, Sum-Set, and Power-Set Axioms......Page 188 5 Pairing and Finiteness Axioms......Page 189 6 Bringing Individuals into Set Theory: Foundation and Plenitude Axioms......Page 191 7 An In nity Axiom and the Replacement Axioms......Page 192 8 Setting Up Experiments on a Theorem-Prover......Page 194 9 A Case-Study Experiment Run on Otter......Page 196 10 Conclusions......Page 197 References......Page 198 1 Introduction......Page 200 2 Syntax and Semantics of ALB......Page 201 3 The Resolution Framework......Page 203 4 Decidability by Ordered Resolution......Page 204 5 Decidability by Selection......Page 206 6 Simulation of Tableaux for ALC......Page 210 7 Model Generation......Page 212 8 Conclusion......Page 213 References......Page 214 1 Introduction......Page 215 2 Preliminaries......Page 216 3 Disequation Normal Form......Page 218 4 A Resolution-Based Calculus in c-Clause Logic......Page 220 5.1 Unification Revisited......Page 222 5.2 Multiset Orderings......Page 223 6 Extension of Decision Classes to c-Clause Logic......Page 226 References......Page 228 1 Introduction......Page 230 2.1 Equational Problems and Constrained Clauses......Page 232 2.2 A Rule System on Constrained Clauses......Page 233 2.3 Semantic Trees in c-clause Logic......Page 234 3 Complete Inference Systems......Page 235 4 Subsumption on Standard Clauses......Page 238 5 Ordering-Based Redundancy Criteria......Page 240 6 Concluding Remarks and Future Work......Page 243 References......Page 244 1 Introduction......Page 245 2 Gentzen-Type Calculi for Intuitionistic Modal Logics Considered......Page 247 3 Cut-Free Indexed Calculi......Page 250 4 Admissibility of the Cut Rule in Indexed Calculi......Page 252 5 Harrop Properties......Page 256 6 Analogue of the Interpolation Property......Page 258 References......Page 259 1 Introduction......Page 260 2 Hidden Algebra......Page 261 3 Rules of Inference......Page 264 3.1 Coinduction and Cobases......Page 266 4 Proving Congruence......Page 269 4.1 A Congruence Criterion......Page 271 5 Reducing the Behavioral Operations......Page 272 References......Page 274 1 Introduction......Page 276 2.3 Many-Valued Logics......Page 277 3 SH_n -Logics......Page 278 3.1 Algebraic Semantics for Propositional SH_n-Logics......Page 279 3.2 A Finite Kripke-Style Frame for SH_n-Logics......Page 280 4 Translation into Clause Form......Page 281 5 Automated Theorem Proving......Page 286 6 Comparison with Other Methods......Page 288 7 Conclusions......Page 289 References......Page 290 Author Index......Page 308 Thisvolumeisacollectionofpapers Onautomateddeduction Inclassical,modal, And Many-valued Logics, With An Emphasis On Rst-order Theories. Some Authors Bridgethe Gaptohigher-order Logicbydealingwithsimpletype Theory Ina R- Order Setting, Or By Resolving Shortcomings Of R St-order Logic With The Help Of Higher-order Notions. Most Papers Rely On Resolution Or Tableaux Methods, With A Few Exceptions Choosing The Equational Paradigm. In Its Entirety The Volume Is A Mirror Of Contemporary Research In R St-order Theorem Proving. One Trend To Be Observed Is The Interest In E Ective Decision Procedures. The Main Aim Of Rs T-order Theorem Proving Was And Still Is To Demonstrate The Validity Or Unsatisa Bility Of Formulas, By More And More - Phisticatedmethods. Withinthelastyears,however,theothersideofthemedal{ Falsi Abilityand Satisab Ility { Has R Eceived Growing Attention. Though In G- Eral Non-terminating, Theorem Provers Sometimes Act As Decision Procedures On Subclasses Ofrs T-order Logic. Inparticularcases Theiroutputcanevenbeused To Extract N Ite Representations Of Models Or Counter-examples. Another Devel- Mentistheextension Ofdeductiontechniquesfromclassicallogictomany-valued And Modal Logics. By Suitably Generalizing Classical Concepts Many Results Carry Over To Non-classical Logics. This Line Of Research Is Stimulated By Artici Al Int- Ligence With Its Need For More Expressive Logics Capable Of Modeling Real-world Reasoning. From A Formal Point Of View This Volume Comprises Two Types Of Papers, Invited And Contributed Ones. Gilles Dowek, Melvin Fitting, Deepak Kapur, Alexander Leitsch, And David Plaisted Accepted Our Invitation To Present Recent Developments In And Their View Of The E Ld. Contributed Papers On The Other Hand Underwent A Two-staged Selection Process. Invited Papers -- 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 -- Contributed Papers -- 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 ((n · Log N)3)-time Transformation From Grz Into Decidable Fragments Of Classical First-order Logic -- 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 N-logics -- Full First-order Sequent And Tableau Calculi With Preservation Of Solutions And The Liberalized ?-rule But Without Skolemization. Ricardo Caferra, Gernot Salzer (eds.). Includes Bibliographical References And Index. This title presents papers reflecting the status of research in automated deduction in classical and non-classical logics. Most of the results presented rely on resolution or tableaux methods with a few exceptions choosing the equational paradigm.