Notice bibliographique
- Notice
Type(s) de contenu et mode(s) de consultation : Texte noté : électronique
Auteur(s) : IJCAR Conference (6 ; 2012 ; Manchester, England)
Titre(s) : Automated reasoning [Texte électronique] : 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings / Bernhard Gramlich, Dale Miller, Uli Sattler (eds.)
Publication : Berlin ; New York : Springer, [2012]
Description matérielle : 1 ressource dématérialisée
Collection : Lecture notes in computer science ; 7364. Lecture notes in artificial intelligence
LNCS sublibrary. SL 7, Artificial intelligence
Note(s) : International conference proceedings. - Includes bibliographical references and author index
Autre(s) auteur(s) : Gramlich, Bernhard (Dr.rer.nat.). Fonction indéterminée
Miller, Dale A.. Fonction indéterminée
Sattler, Uli. Fonction indéterminée
Autre(s) forme(s) du titre :
- Autre forme du titre : IJCAR 2012
Sujet(s) : Théorèmes -- Démonstration automatique
Logique informatique
Indice(s) Dewey : 511.360 28563 (23e éd.) = Démonstration automatique de théorèmes
Identifiants, prix et caractéristiques : ISBN 9783642313653
Identifiant de la notice : ark:/12148/cb44704970v
Notice n° :
FRBNF44704970
(notice reprise d'un réservoir extérieur)
Table des matières : 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?
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, J
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-Schauß ; Fingerprint
Indexing for Paramodulation and