Return to home page
Searching: Baldwin Wallace library catalog
We are currently experiencing delivery delays for items requested from other institutions while transitioning to a new statewide delivery service. Please contact your library with questions or advice about alternative resources. Thank you for your patience!
  Previous Record Previous Item Next Item Next Record
  Reviews, Summaries, etc...
EBOOK
Title Automated deduction in classical and non-classical logics : selected papers / Ricardo Caferra, Gernot Salzer (eds.).
Imprint Berlin ; New York : Springer, 2000.

LOCATION CALL # STATUS MESSAGE
 OHIOLINK SPRINGER EBOOKS    ONLINE  
View online
LOCATION CALL # STATUS MESSAGE
 OHIOLINK SPRINGER EBOOKS    ONLINE  
View online
Series Lecture notes in computer science ; 1761. Lecture notes in artificial intelligence.
Lecture notes in computer science. Lecture notes in artificial intelligence.
Subject Automatic theorem proving.
Logic, Symbolic and mathematical.
Alt Name Caferra, Ricardo, 1945-
Salzer, Gernot, 1963-
Ohio Library and Information Network.
Description viii, 297 pages : illustrations ; 23 cm.
Bibliography Note Includes bibliographical references and index.
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((nlog n)³)-time transformation from Grz into decidable fragments of classical first-order logic / Stephane Demri, Rajeev Gore -- Implicational completeness of signed resolution / Christian G. Fermuller -- 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 Pliuskeviciene -- Hidden congruent deduction / Grigore Rosu, 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.
Access Available to OhioLINK libraries
Summary 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.
Reproduction Electronic reproduction. Columbus, OH : OhioLINK, 2008.
System Details Mode of access: World Wide Web
ISBN 3540671900 (softcover : alk. paper)
9783540671909 (softcover : alk. paper)
OCLC # 644339773
Link OhioLINK electronic book center (OCoLC)180989150.
SpringerLink (OCoLC)43927870.
Additional Format Print version: Automated deduction in classical and non-classical logics. Berlin ; New York : Springer, 2000 3540671900 (DLC) 00028492 (OCoLC)43599196.



If you experience difficulty accessing or navigating this content, please contact the OPAL Support Team