Automated Deduction in Classical and Non-Classical Logics [[electronic resource] ] : Selected Papers / / edited by Ricardo Caferra, Gernot Salzer
(Visualizza in formato marc)
(Visualizza in BIBFRAME)
| Titolo: |
Automated Deduction in Classical and Non-Classical Logics [[electronic resource] ] : Selected Papers / / edited by Ricardo Caferra, Gernot Salzer
|
| Pubblicazione: | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
| Edizione: | 1st ed. 2000. |
| Descrizione fisica: | 1 online resource (VIII, 304 p.) |
| Disciplina: | 006.3/33 |
| Soggetto topico: | Artificial intelligence |
| Mathematical logic | |
| Computer logic | |
| Artificial Intelligence | |
| Mathematical Logic and Formal Languages | |
| Logics and Meanings of Programs | |
| Persona (resp. second.): | CaferraRicardo |
| SalzerGernot | |
| Note generali: | Bibliographic Level Mode of Issuance: Monograph |
| Nota di bibliografia: | Includes bibliographical references and index. |
| Nota di contenuto: | 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. |
| Titolo autorizzato: | Automated deduction in classical and non-classical logics |
| ISBN: | 3-540-46508-1 |
| Formato: | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione: | Inglese |
| Record Nr.: | 9910143638903321 |
| Lo trovi qui: | Univ. Federico II |
| Opac: | Controlla la disponibilità qui |
Serie:
Lecture Notes in Artificial Intelligence ; ; 1761