Automated deduction in classical and non-classical logics : selected papers /
| Corporate Author: | |
|---|---|
| Other Authors: | , |
| Format: | eBook |
| Language: | English |
| Published: |
Berlin ; New York :
Springer,
2000.
|
| Series: | Lecture notes in computer science ;
1761. Lecture notes in computer science. Lecture notes in artificial intelligence. |
| Subjects: | |
| Online Access: | Connect to the full text of this electronic book |
Table of Contents:
- Automated theorem proving in first-order logic modulo : on the difference between type theory and set theory / Gilles Dowek
- Higher-order modal logic--a sketch / Melvin Fitting
- Proving associative-commutative termination using RPO-compatible orderings / Deepak Kapur, G. Sivakumar
- Decision procedures and model building, or how to improve logical information in automated deduction / Alexander Leitsch
- Replacement rules with definition detection / David A. Plaisted, Yunshan Zhu
- On the comlexity [sic] of finite sorted algebras / Thierry Boy de la Tour
- A further and effective liberalization of the [delta]-rule in free variable sematic tableaux / Domenico Cantone, Marianna Nicolosi Asmundo
- A new fast tableau-based decision procedure for an unquantified fragment of set theory / Domenico Cantone, Calogero G. Zarba
- Interpretation of a Mizar-like logic in first-order logic / Ingo Dahn
- An O((n·log n)³)-time transformation from Grz into decidable fragments of classical first-order logic / Stéphane Demri, Rajeev Goré
- Implicational completeness of signed resolution / Christian G. Fermüller
- An equational re-engineering of set theories / Andrea Fromisano, Eugenio Omodeo
- Issues of decidability for description logics in the framework of resolution / Ullrich Hustadt, Renate A. Schmidt
- Extending decidable clause classes via constraints / Reinhard Pichler
- Completeness and redundancy in constrained clause logic / Reinhard Pichler
- Effective properties of some first-order intuitionistic modal logics / Aida Pliuškevičienė
- Hidden congruent deduction / Grigore Roșu, Joseph Goguen
- Resolution-based theorem proving for SH[subscript n]-logics / Viorica Sofronie-Stokkermans
- Full first-order sequent and tableau calculi with preservation of solutions and the liberalized [delta]-rule but without skolemization / Claus-Peter Wirth.