FEEDBACK Smiley face
Normal view MARC view ISBD view

Automated Deduction in Classical and Non-Classical Logics [electronic resource] :Selected Papers /

Contributor(s): Caferra, Ricardo [editor.] | Salzer, Gernot [editor.] | SpringerLink (Online service).
Material type: materialTypeLabelBookSeries: Lecture Notes in Computer Science: 1761Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg, 2000.Description: VIII, 304 p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9783540465089.Subject(s): Computer science | Computer logic | Mathematical logic | Artificial intelligence | Computer Science | Artificial Intelligence (incl. Robotics) | Mathematical Logic and Formal Languages | Logics and Meanings of ProgramsOnline resources: Click here to access online
Contents:
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.
In: Springer eBooks
Tags from this library: No tags from this library for this title. Add tag(s)
Log in to add tags.
    average rating: 0.0 (0 votes)
No physical items for this record

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.

There are no comments for this item.

Log in to your account to post a comment.

© IIIT-Delhi, 2013 | Phone: +91-11-26907510| FAX +91-11-26907405 | E-mail: library@iiitd.ac.in