000 06325nam a22006255i 4500
001 978-3-540-71070-7
003 DE-He213
005 20240423125802.0
007 cr nn 008mamaa
008 100301s2008 gw | s |||| 0|eng d
020 _a9783540710707
_9978-3-540-71070-7
024 7 _a10.1007/978-3-540-71070-7
_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 Reasoning
_h[electronic resource] :
_b4th International Joint Conference, IJCAR 2008, Sydney, NSW, Australia, August 12-15, 2008, Proceedings /
_cedited by Alessandro Armando, Peter Baumgartner, Gilles Dowek.
250 _a1st ed. 2008.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2008.
300 _aXII, 556 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 ;
_v5195
505 0 _aSession 1: Invited Talk -- Software Verification: Roles and Challenges for Automatic Decision Procedures -- Session 2: Specific Theories -- Proving Bounds on Real-Valued Functions with Computations -- Linear Quantifier Elimination -- Quantitative Separation Logic and Programs with Lists -- On Automating the Calculus of Relations -- Session 3: Automated Verification -- Towards SMT Model Checking of Array-Based Systems -- Preservation of Proof Obligations from Java to the Java Virtual Machine -- Efficient Well-Definedness Checking -- Session 4: Protocol Verification -- Proving Group Protocols Secure Against Eavesdroppers -- Session 5: System Descriptions 1 -- Automated Implicit Computational Complexity Analysis (System Description) -- LogAnswer - A Deduction-Based Question Answering System (System Description) -- A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description) -- The Abella Interactive Theorem Prover (System Description) -- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) -- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) -- The Complexity of Conjunctive Query Answering in Expressive Description Logics -- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments -- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse -- Session 8: Herbrand Award Ceremony -- Automata-Based Axiom Pinpointing -- Individual Reuse in Description Logic Reasoning -- The Logical Difference Problem for Description Logic Terminologies -- Session 10: System Descriptions 2 -- Aligator: A Mathematica Package for Invariant Generation (System Description) -- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) -- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description) -- An Experimental Evaluation of Global Caching for (System Description) -- Multi-completion with Termination Tools (System Description) -- MTT: The Maude Termination Tool (System Description) -- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) -- Canonicity! -- Unification and Matching Modulo Leaf-Permutative Equational Presentations -- Modularity of Confluence -- Automated Complexity Analysis Based on the Dependency Pair Method -- Canonical Inference for Implicational Systems -- Challenges in the Automated Verification of Security Protocols -- Session 14: Theorem Proving 1 -- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets -- Proof Systems for Effectively Propositional Logic -- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance -- CASC-J4 The 4th IJCAR ATP System Competition -- Session 16: Theorem Proving 2 -- Labelled Splitting -- Engineering DPLL(T) + Saturation -- THF0 – The Core of the TPTP Language for Higher-Order Logic -- Focusing in Linear Meta-logic -- Certifying a Tree Automata Completion Checker -- Automated Induction with Constrained Tree Automata.
520 _aThis book constitutes the refereed proceedings of the 4th International Joint Conference on Automated Reasoning, IJCAR 2008, held in Sydney, Australia, in August 2008. The 26 revised full research papers and 13 revised system descriptions presented together with 4 invited papers and a summary of the CASC-J4 systems competition were carefully reviewed and selected from 80 full paper and 17 system description submissions. The papers address the entire spectrum of research in automated reasoning and are organized in topical sections on specific theories, automated verification, protocol verification, system descriptions, modal logics, description logics, equational theories, theorem proving, CASC, the 4th IJCAR ATP system competition, logical frameworks, and tree automata.
650 0 _aArtificial intelligence.
650 0 _aSoftware engineering.
650 0 _aComputer programming.
650 0 _aMachine theory.
650 0 _aComputer science.
650 1 4 _aArtificial Intelligence.
650 2 4 _aSoftware Engineering.
650 2 4 _aProgramming Techniques.
650 2 4 _aFormal Languages and Automata Theory.
650 2 4 _aComputer Science Logic and Foundations of Programming.
700 1 _aArmando, Alessandro.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aBaumgartner, Peter.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aDowek, Gilles.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540710691
776 0 8 _iPrinted edition:
_z9783540867494
830 0 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v5195
856 4 0 _uhttps://doi.org/10.1007/978-3-540-71070-7
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cSPRINGER
999 _c181687
_d181687