LEADER 08957nam 22008295 450 001 996465531903316 005 20200704035205.0 010 $a3-642-31365-5 024 7 $a10.1007/978-3-642-31365-3 035 $a(CKB)3400000000085357 035 $a(SSID)ssj0000697451 035 $a(PQKBManifestationID)11481602 035 $a(PQKBTitleCode)TC0000697451 035 $a(PQKBWorkID)10709325 035 $a(PQKB)10357989 035 $a(DE-He213)978-3-642-31365-3 035 $a(MiAaPQ)EBC3070155 035 $a(PPN)168319195 035 $a(EXLCZ)993400000000085357 100 $a20120621d2012 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Reasoning$b[electronic resource] $e6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings /$fedited by Bernhard Gramlich, Dale Miller, Ulrike Sattler 205 $a1st ed. 2012. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2012. 215 $a1 online resource (XIV, 568 p. 90 illus.) 225 1 $aLecture Notes in Artificial Intelligence ;$v7364 300 $aInternational conference proceedings. 311 $a3-642-31364-7 320 $aIncludes bibliographical references and author index. 327 $tTaking Satisfiability to the Next Level with Z3$g(Abstract) /$rNikolaj Bjørner --$tEnlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics /$rYuri Matiyasevich --$tSAT and SMT Are Still Resolution: Questions and Challenges /$rRobert Nieuwenhuis --$tUnification Modulo Synchronous Distributivity /$rSiva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran and Michael Rusinowitch --$tSAT Encoding of Unification in ELHR+R+ w.r.t. Cycle-Restricted Ontologies /$rFranz Baader, Stefan Borgwardt and Barbara Morawska --$tUEL: Unification Solver for the Description Logic EL -- System Description /$rFranz Baader, Julian Mendez and Barbara Morawska --$tEffective Finite-Valued Semantics for Labelled Calculi /$rMatthias Baaz, Ori Lahav and Anna Zamansky --$tA Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic /$rFranc?ois Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala and Assia Mahboubi, et al. --$tHow Fuzzy Is My Fuzzy Description Logic? /$rStefan Borgwardt, Felix Distel and Rafael Pen?aloza --$tTruthful Monadic Abstractions /$rTaus Brock-Nannestad and Carsten Schu?rmann --$tSatallax: An Automatic Higher-Order Prover /$rChad E. Brown --$tFrom Strong Amalgamability to Modularity of Quantifier-Free Interpolation /$rRoberto Bruttomesso, Silvio Ghilardi and Silvio Ranise --$tSPARQL Query Containment under RDFS Entailment Regime /$rMelisachew Wudage Chekol, Je?ro?me Euzenat, Pierre Geneve?s and Nabil Layai?da. 327 $tAutomated Verification of Recursive Programs with Pointers /$rFrank de Boer, Marcello Bonsangue and Jurriaan Rot --$tSecurity Protocols, Constraint Systems, and Group Theories /$rSte?phanie Delaune, Steve Kremer and Daniel Pasaila --$tTaming Past LTL and Flat Counter Systems /$rSte?phane Demri, Amit Kumar Dhar and Arnaud Sangnier --$tA Calculus for Generating Ground Explanations /$rMnacho Echenim and Nicolas Peltier --$tEPR-Based Bounded Model Checking at Word Level /$rMoshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel and Andrei Voronkov --$tProving Non-looping Non-termination Automatically /$rFabian Emmes, Tim Enger and Ju?rgen Giesl --$tRewriting Induction + Linear Arithmetic = Decision Procedure /$rStephan Falke and Deepak Kapur --$tCombination of Disjoint Theories: Beyond Decidability /$rPascal Fontaine, Stephan Merz and Christoph Weidenbach --$tAutomated Analysis of Regular Algebra /$rSimon Foster and Georg Struth --$t[delta]-Complete Decision Procedures for Satisfiability over the Reals /$rSicun Gao, Jeremy Avigad and Edmund M. Clarke --$tBDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics /$rRajeev Gore? and Jimmy Thomson --$tFrom Linear Temporal Logic Properties to Rewrite Propositions /$rPierre-Cyrille He?am, Vincent Hugot and Olga Kouchnarenko --$tTableaux Modulo Theories Using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover /$rMe?lanie Jacquel, Karim Berkani, David Delahaye and Catherine Dubois. 327 $tSolving Non-linear Arithmetic /$rDejan Jovanovic? and Leonardo de Moura --$tInprocessing Rules /$rMatti Ja?rvisalo, Marijn J.H. Heule and Armin Biere --$tLogical Difference Computation with CEX2.5 /$rBoris Konev, Michel Ludwig and Frank Wolter --$tOverview and Evaluation of Premise Selection Techniques for Large Theory Mathematics /$rDaniel Ku?hlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban and Tom Heskes --$tBranching Time? Pruning Time! /$rMarkus Latte and Martin Lange --$tNew Algorithms for Unification Modulo One-Sided Distributivity and Its Variants /$rAndrew M. Marshall and Paliath Narendran --$tReachability Analysis of Program Variables /$r?urica Nikolic? and Fausto Spoto --$tPlaying Hybrid Games with KeYmaera /$rJan-David Quesel and Andre? Platzer --$tThe QMLTP Problem Library for First-Order Modal Logics /$rThomas Raths and Jens Otten --$tCorrectness of Program Transformations as a Termination Problem /$rConrad Rau, David Sabel and Manfred Schmidt-Schauss --$tFingerprint Indexing for Paramodulation and Rewriting /$rStephan Schulz --$tOptimization in SMT with LAA Q Cost Functions /$rRoberto Sebastiani and Silvia Tomasi --$tSynthesis for Unbounded Bit-Vector Arithmetic /$rAndrej Spielmann and Viktor Kuncak --$tExtended Caching, Backjumping and Merging for Expressive Description Logics /$rAndreas Steigmiller, Thorsten Liebig and Birte Glimm --$tKBCV -- Knuth-Bendix Completion Visualizer /$rThomas Sternagel and Harald Zankl --$tA PLTL-Prover Based on Labelled Superposition with Partial Model Guidance /$rMartin Suda and Christoph Weidenbach --$tStratification in Logics of Definitions /$rAlwen Tiu --$tDiabelli: A Heterogeneous Proof System /$rMatej Urbas and Mateja Jamnik. 330 $aThis book constitutes the refereed proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR 2012, held in Manchester, UK, in June 2012. IJCAR 2012 is a merger of leading events in automated reasoning, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), FTP (International Workshop on First-Order Theorem Proving), and TABLEAUX (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods). The 32 revised full research papers and 9 system descriptions presented together with 3 invited talks were carefully reviewed and selected from 116 submissions. The papers address all aspects of automated reasoning, including foundations, implementations, and applications. 410 0$aLecture Notes in Artificial Intelligence ;$v7364 606 $aMathematical logic 606 $aComputer logic 606 $aArtificial intelligence 606 $aSoftware engineering 606 $aComputer science?Mathematics 606 $aNumerical analysis 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aMathematics of Computing$3https://scigraph.springernature.com/ontologies/product-market-codes/I17001 606 $aNumeric Computing$3https://scigraph.springernature.com/ontologies/product-market-codes/I1701X 608 $aConference papers and proceedings.$2fast 615 0$aMathematical logic. 615 0$aComputer logic. 615 0$aArtificial intelligence. 615 0$aSoftware engineering. 615 0$aComputer science?Mathematics. 615 0$aNumerical analysis. 615 14$aMathematical Logic and Formal Languages. 615 24$aLogics and Meanings of Programs. 615 24$aArtificial Intelligence. 615 24$aSoftware Engineering. 615 24$aMathematics of Computing. 615 24$aNumeric Computing. 676 $a511.3/6028563 702 $aGramlich$b Bernhard$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aMiller$b Dale$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSattler$b Ulrike$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aIJCAR (Conference) 906 $aBOOK 912 $a996465531903316 996 $aAutomated Reasoning$9771895 997 $aUNISA