Format:
Online-Ressource
ISBN:
9783540465089
,
3540671900
Series Statement:
Lecture Notes in Computer Science 1761
Content:
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.
Note:
Lizenzpflichtig
Additional Edition:
ISBN 9783540671909
Additional Edition:
Buchausg. u.d.T. Automated deduction in classical and non-classical logics Berlin : Springer, 2000 ISBN 3540671900
Language:
English
Keywords:
Automatisches Beweisverfahren
;
Prädikatenlogik
;
Stufe 1
;
Aufsatzsammlung
;
Konferenzschrift
DOI:
10.1007/3-540-46508-1
URL:
Volltext
(lizenzpflichtig)
URL:
Volltext
(lizenzpflichtig)
Author information:
Caferra, Ricardo 1945-
