Automated Reasoning [[electronic resource] ] : 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings / / edited by Bernhard Gramlich, Dale Miller, Ulrike Sattler

• Pubblicazione: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012
• Edizione: 1st ed. 2012.
• Descrizione fisica: 1 online resource (XIV, 568 p. 90 illus.)
• Disciplina: 511.3/6028563
• Soggetto topico: Mathematical logic; Computer logic; Artificial intelligence; Software engineering; Computer science—Mathematics; Numerical analysis; Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Artificial Intelligence; Software Engineering; Mathematics of Computing; Numeric Computing
• Soggetto genere / forma: Conference papers and proceedings.
• Persona (resp. second.): GramlichBernhard; MillerDale; SattlerUlrike
• Note generali: International conference proceedings.
• Nota di bibliografia: Includes bibliographical references and author index.
• Nota di contenuto: Taking Satisfiability to the Next Level with Z3 ; (Abstract) / Nikolaj Bjørner -- Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics / Yuri Matiyasevich -- SAT and SMT Are Still Resolution: Questions and Challenges / Robert Nieuwenhuis -- Unification Modulo Synchronous Distributivity / Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran and Michael Rusinowitch -- SAT Encoding of Unification in ELHR+R+ w.r.t. Cycle-Restricted Ontologies / Franz Baader, Stefan Borgwardt and Barbara Morawska -- UEL: Unification Solver for the Description Logic EL -- System Description / Franz Baader, Julian Mendez and Barbara Morawska -- Effective Finite-Valued Semantics for Labelled Calculi / Matthias Baaz, Ori Lahav and Anna Zamansky -- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic / François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala and Assia Mahboubi, et al. -- How Fuzzy Is My Fuzzy Description Logic? / Stefan Borgwardt, Felix Distel and Rafael Peñaloza -- Truthful Monadic Abstractions / Taus Brock-Nannestad and Carsten Schürmann -- Satallax: An Automatic Higher-Order Prover / Chad E. Brown -- From Strong Amalgamability to Modularity of Quantifier-Free Interpolation / Roberto Bruttomesso, Silvio Ghilardi and Silvio Ranise -- SPARQL Query Containment under RDFS Entailment Regime / Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès and Nabil Layaïda. ; Automated Verification of Recursive Programs with Pointers / Frank de Boer, Marcello Bonsangue and Jurriaan Rot -- Security Protocols, Constraint Systems, and Group Theories / Stéphanie Delaune, Steve Kremer and Daniel Pasaila -- Taming Past LTL and Flat Counter Systems / Stéphane Demri, Amit Kumar Dhar and Arnaud Sangnier -- A Calculus for Generating Ground Explanations / Mnacho Echenim and Nicolas Peltier -- EPR-Based Bounded Model Checking at Word Level / Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel and Andrei Voronkov -- Proving Non-looping Non-termination Automatically / Fabian Emmes, Tim Enger and Jürgen Giesl -- Rewriting Induction + Linear Arithmetic = Decision Procedure / Stephan Falke and Deepak Kapur -- Combination of Disjoint Theories: Beyond Decidability / Pascal Fontaine, Stephan Merz and Christoph Weidenbach -- Automated Analysis of Regular Algebra / Simon Foster and Georg Struth -- [delta]-Complete Decision Procedures for Satisfiability over the Reals / Sicun Gao, Jeremy Avigad and Edmund M. Clarke -- BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics / Rajeev Goré and Jimmy Thomson -- From Linear Temporal Logic Properties to Rewrite Propositions / Pierre-Cyrille Héam, Vincent Hugot and Olga Kouchnarenko -- Tableaux Modulo Theories Using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover / Mélanie Jacquel, Karim Berkani, David Delahaye and Catherine Dubois. ; Solving Non-linear Arithmetic / Dejan Jovanović and Leonardo de Moura -- Inprocessing Rules / Matti Järvisalo, Marijn J.H. Heule and Armin Biere -- Logical Difference Computation with CEX2.5 / Boris Konev, Michel Ludwig and Frank Wolter -- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics / Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban and Tom Heskes -- Branching Time? Pruning Time! / Markus Latte and Martin Lange -- New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants / Andrew M. Marshall and Paliath Narendran -- Reachability Analysis of Program Variables / Đurica Nikolić and Fausto Spoto -- Playing Hybrid Games with KeYmaera / Jan-David Quesel and André Platzer -- The QMLTP Problem Library for First-Order Modal Logics / Thomas Raths and Jens Otten -- Correctness of Program Transformations as a Termination Problem / Conrad Rau, David Sabel and Manfred Schmidt-Schauss -- Fingerprint Indexing for Paramodulation and Rewriting / Stephan Schulz -- Optimization in SMT with LAA Q Cost Functions / Roberto Sebastiani and Silvia Tomasi -- Synthesis for Unbounded Bit-Vector Arithmetic / Andrej Spielmann and Viktor Kuncak -- Extended Caching, Backjumping and Merging for Expressive Description Logics / Andreas Steigmiller, Thorsten Liebig and Birte Glimm -- KBCV -- Knuth-Bendix Completion Visualizer / Thomas Sternagel and Harald Zankl -- A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance / Martin Suda and Christoph Weidenbach -- Stratification in Logics of Definitions / Alwen Tiu -- Diabelli: A Heterogeneous Proof System / Matej Urbas and Mateja Jamnik.
• Sommario/riassunto: This 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.
• Titolo autorizzato: Automated Reasoning
• ISBN: 3-642-31365-5
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 996465531903316
• Lo trovi qui: Univ. di Salerno
• Serie: Lecture Notes in Artificial Intelligence ; ; 7364