Automated Deduction in Classical and Non-Classical Logics Selected Papers /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2000.
|
| Έκδοση: | 1st ed. 2000. |
| Σειρά: | Lecture Notes in Artificial Intelligence ;
1761 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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.
