Automated Deduction in Classical and Non-Classical Logics, Selected Papers - researchr publication

researchr

You are not signed in
Sign in
Sign up

Ricardo Caferra, Gernot Salzer, editors, Automated Deduction in Classical and Non-Classical Logics, Selected Papers. Volume 1761 of Lecture Notes in Computer Science, Springer, 2000.

Conference: ftp2000

Abstract is missing.

Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set TheoryGilles Dowek. 1-22 [doi]

Higher-Order Modal Logic - A SketchMelvin Fitting. 23-38 [doi]

Proving Associative-Communicative Termination Using RPO-Compatible OrderingsDeepak Kapur, G. Sivakumar. 39-61 [doi]

Decision Procedures and Model Building, or How to Improve Logical Information in Automated DeductionAlexander Leitsch. 62-79 [doi]

Replacement Rules with Definition DetectionDavid A. Plaisted, Yunshan Zhu. 80-94 [doi]

On the Complexity of Finite Sorted AlgebrasThierry Boy de la Tour. 95-108 [doi]

A Further and Effective Liberalization of the delta-Rule in Free Variable Semantic TableauxDomenico Cantone, Marianna Nicolosi Asmundo. 109-125 [doi]

A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set TheoryDomenico Cantone, Calogero G. Zarba. 126-136 [doi]

Interpretation of a Mizar-Like Logic in First-Order LogicIngo Dahn. 137-151 [doi]

An O ((::::n::::·log ::::n::::):::3:::)-Time Transformation from Grz into Decidable Fragments of Classical First-Order LogicStéphane Demri, Rajeev Goré. 152-166 [doi]

Implicational Completeness of Signed ResolutionChristian G. Fermüller. 167-174 [doi]

An Equational Re-engineering of Set TheoriesAndrea Formisano, Eugenio G. Omodeo. 175-190 [doi]

Issues of Decidability for Description Logics in the Framework of ResolutionUllrich Hustadt, Renate A. Schmidt. 191-205 [doi]

Extending Decidable Clause Classes via ConstraintsReinhard Pichler. 206-220 [doi]

Completeness and Redundancy in Constrained Clause LogicReinhard Pichler. 221-235 [doi]

Effective Properties of Some First-Order Intuitionistic Modal LogicsAida Pliuskeviciene. 236-250 [doi]

Hidden Congruent DeductionGrigore Rosu, Joseph A. Goguen. 251-266 [doi]

Resolution-Based Theorem Proving for ::::SH::n::::::-LogicsViorica Sofronie-Stokkermans. 267-281 [doi]

Full First-Order Sequent and Tableau Calculi with Preservation of Solutions and the Liberalized delta-Rule but without SkolemizationClaus-Peter Wirth. 282-297 [doi]

runs on WebDSL