000 | 03583nam a22005295i 4500 | ||
---|---|---|---|
001 | 978-3-540-45616-2 | ||
003 | DE-He213 | ||
005 | 20160624102005.0 | ||
007 | cr nn 008mamaa | ||
008 | 121227s2002 gw | s |||| 0|eng d | ||
020 |
_a9783540456162 _9978-3-540-45616-2 |
||
024 | 7 |
_a10.1007/3-540-45616-3 _2doi |
|
050 | 4 | _aQ334-342 | |
050 | 4 | _aTJ210.2-211.495 | |
072 | 7 |
_aUYQ _2bicssc |
|
072 | 7 |
_aTJFM1 _2bicssc |
|
072 | 7 |
_aCOM004000 _2bisacsh |
|
082 | 0 | 4 |
_a006.3 _223 |
245 | 1 | 0 |
_aAutomated Reasoning with Analytic Tableaux and Related Methods _h[electronic resource] : _bInternational Conference, TABLEAUX 2002 Copenhagen, Denmark, July 30 – August 1, 2002 Proceedings / _cedited by Uwe Egly, Chritian G. Fermüller. |
260 | 1 |
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c2002. |
|
264 | 1 |
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c2002. |
|
300 |
_aX, 346 p. _bonline resource. |
||
336 |
_atext _btxt _2rdacontent |
||
337 |
_acomputer _bc _2rdamedia |
||
338 |
_aonline resource _bcr _2rdacarrier |
||
347 |
_atext file _bPDF _2rda |
||
490 | 1 |
_aLecture Notes in Computer Science, _x0302-9743 ; _v2381 |
|
505 | 0 | _aInvited Papers -- Proof Analysis by Resolution -- Using Linear Logic to Reason about Sequent Systems -- Research Papers -- A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic -- Tableaux for Quantified Hybrid Logic -- Tableau-Based Automated Deduction for Duration Calculus -- Linear Time Logic, Conditioned Models, and Planning with Incomplete Knowledge -- A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic -- Modal Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks -- Tableau Calculi for the Logics of Finite k-Ary Trees -- A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition -- Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment -- Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas -- Integration of Equality Reasoning into the Disconnection Calculus -- Analytic Sequent Calculi for Abelian and ?ukasiewicz Logics -- Analytic Tableau Systems for Propositional Bimodal Logics of Knowledge and Belief -- A Confluent Theory Connection Calculus -- On Uniform Word Problems Involving Bridging Operators on Distributive Lattices -- Question Answering: From Partitions to Prolog -- A General Theorem Prover for Quantified Modal Logics -- Some New Exceptions for the Semantic Tableaux Version of the Second Incompleteness Theorem -- A New Indefinite Semantics for Hilbert’s Epsilon -- A Tableau Calculus for Combining Non-disjoint Theories -- System Descriptions Papers -- LINK: A Proof Environment Based on Proof Nets -- DCTP 1.2 — System Abstract. | |
650 | 0 | _aComputer science. | |
650 | 0 | _aSoftware engineering. | |
650 | 0 | _aArtificial intelligence. | |
650 | 1 | 4 | _aComputer Science. |
650 | 2 | 4 | _aArtificial Intelligence (incl. Robotics). |
650 | 2 | 4 | _aMathematical Logic and Formal Languages. |
650 | 2 | 4 | _aSoftware Engineering. |
650 | 2 | 4 | _aProgramming Techniques. |
700 | 1 |
_aEgly, Uwe. _eeditor. |
|
700 | 1 |
_aFermüller, Chritian G. _eeditor. |
|
710 | 2 | _aSpringerLink (Online service) | |
773 | 0 | _tSpringer eBooks | |
776 | 0 | 8 |
_iPrinted edition: _z9783540439295 |
786 | _dSpringer | ||
830 | 0 |
_aLecture Notes in Computer Science, _x0302-9743 ; _v2381 |
|
856 | 4 | 0 | _uhttp://dx.doi.org/10.1007/3-540-45616-3 |
942 |
_2EBK5479 _cEBK |
||
999 |
_c34773 _d34773 |