| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996465531903316 |
|
|
Titolo |
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 |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2012.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XIV, 568 p. 90 illus.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Artificial Intelligence ; ; 7364 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
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 |
Conference papers and proceedings. |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
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. |
|
|
|
|
|
|
|
| |