000 | 03915nam a22005655i 4500 | ||
---|---|---|---|
001 | 978-3-540-31864-4 | ||
003 | DE-He213 | ||
005 | 20240730190549.0 | ||
007 | cr nn 008mamaa | ||
008 | 100721s2005 gw | s |||| 0|eng d | ||
020 |
_a9783540318644 _9978-3-540-31864-4 |
||
024 | 7 |
_a10.1007/11532231 _2doi |
|
050 | 4 | _aQ334-342 | |
050 | 4 | _aTA347.A78 | |
072 | 7 |
_aUYQ _2bicssc |
|
072 | 7 |
_aCOM004000 _2bisacsh |
|
072 | 7 |
_aUYQ _2thema |
|
082 | 0 | 4 |
_a006.3 _223 |
245 | 1 | 0 |
_aAutomated Deduction - CADE-20 _h[electronic resource] : _b20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings / _cedited by Robert Nieuwenhuis. |
250 | _a1st ed. 2005. | ||
264 | 1 |
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg : _bImprint: Springer, _c2005. |
|
300 |
_aXIV, 466 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 Artificial Intelligence, _x2945-9141 ; _v3632 |
|
505 | 0 | _aWhat Do We Know When We Know That a Theory Is Consistent? -- Reflecting Proofs in First-Order Logic with Equality -- Reasoning in Extensional Type Theory with Equality -- Nominal Techniques in Isabelle/HOL -- Tabling for Higher-Order Logic Programming -- A Focusing Inverse Method Theorem Prover for First-Order Linear Logic -- The CoRe Calculus -- Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures -- Privacy-Sensitive Information Flow with JML -- The Decidability of the First-Order Theory of Knuth-Bendix Order -- Well-Nested Context Unification -- Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules -- The OWL Instance Store: System Description -- Temporal Logics over Transitive States -- Deciding Monodic Fragments by Temporal Resolution -- Hierarchic Reasoning in Local Theory Extensions -- Proof Planning for First-Order Temporal Logic -- System Description: Multi A Multi-strategy Proof Planner -- Decision Procedures Customized for Formal Verification -- An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic -- Connecting Many-Sorted Theories -- A Proof-Producing Decision Procedure for Real Arithmetic -- The MathSAT 3 System -- Deduction with XOR Constraints in Security API Modelling -- On the Complexity of Equational Horn Clauses -- A Combination Method for Generating Interpolants -- sKizzo: A Suite to Evaluate and Certify QBFs -- Regular Protocols and Attacks with Regular Knowledge -- The Model Evolution Calculus with Equality -- Model Representation via Contexts and Implicit Generalizations -- Proving Properties of Incremental Merkle Trees -- Computer Search for Counterexamples to Wilkie's Identity -- KRHyper - In Your Pocket. | |
650 | 0 |
_aArtificial intelligence. _93407 |
|
650 | 0 |
_aMachine theory. _9142990 |
|
650 | 0 |
_aComputer science. _99832 |
|
650 | 0 |
_aSoftware engineering. _94138 |
|
650 | 1 | 4 |
_aArtificial Intelligence. _93407 |
650 | 2 | 4 |
_aFormal Languages and Automata Theory. _9142991 |
650 | 2 | 4 |
_aComputer Science Logic and Foundations of Programming. _942203 |
650 | 2 | 4 |
_aSoftware Engineering. _94138 |
700 | 1 |
_aNieuwenhuis, Robert. _eeditor. _4edt _4http://id.loc.gov/vocabulary/relators/edt _9142992 |
|
710 | 2 |
_aSpringerLink (Online service) _9142993 |
|
773 | 0 | _tSpringer Nature eBook | |
776 | 0 | 8 |
_iPrinted edition: _z9783540280057 |
776 | 0 | 8 |
_iPrinted edition: _z9783540813552 |
830 | 0 |
_aLecture Notes in Artificial Intelligence, _x2945-9141 ; _v3632 _9142994 |
|
856 | 4 | 0 | _uhttps://doi.org/10.1007/11532231 |
912 | _aZDB-2-SCS | ||
912 | _aZDB-2-SXCS | ||
912 | _aZDB-2-LNC | ||
942 | _cELN | ||
999 |
_c93322 _d93322 |