default search action
4th IJCAR 2008: Sydney, NSW, Australia
- Alessandro Armando, Peter Baumgartner, Gilles Dowek:
Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. Lecture Notes in Computer Science 5195, Springer 2008, ISBN 978-3-540-71069-1
Invited Talk
- Aarti Gupta:
Software Verification: Roles and Challenges for Automatic Decision Procedures. 1
Specific Theories
- Guillaume Melquiond
:
Proving Bounds on Real-Valued Functions with Computations. 2-17 - Tobias Nipkow
Linear Quantifier Elimination. 18-33 - Marius Bozga, Radu Iosif, Swann Perarnau:
Quantitative Separation Logic and Programs with Lists. 34-49 - Peter Höfner, Georg Struth:
On Automating the Calculus of Relations. 50-66
Automated Verification
- Silvio Ghilardi
Towards SMT Model Checking of Array-Based Systems. 67-82 - Gilles Barthe, Benjamin Grégoire, Mariela Pavlova:
Preservation of Proof Obligations from Java to the Java Virtual Machine. 83-99 - Ádám Darvas, Farhad Mehta, Arsenii Rudich:
Efficient Well-Definedness Checking. 100-115
Protocol Verification
- Steve Kremer
Proving Group Protocols Secure Against Eavesdroppers. 116-131
System Descriptions 1
- Martin Avanzini, Georg Moser, Andreas Schnabl:
Automated Implicit Computational Complexity Analysis (System Description). 132-138 - Ulrich Furbach, Ingo Glöckner, Hermann Helbig, Björn Pelzer:
LogAnswer - A Deduction-Based Question Answering System (System Description). 139-146 - Christoph Beierle, Gabriele Kern-Isberner, Nicole Koch:
A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description). 147-153 - Andrew Gacek:
The Abella Interactive Theorem Prover (System Description). 154-161 - Christoph Benzmüller
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). 162-170 - André Platzer
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). 171-178
Invited Talk
- Carsten Lutz
The Complexity of Conjunctive Query Answering in Expressive Description Logics. 179-193
Modal Logics
- Renate A. Schmidt
A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. 194-209 - Mark Kaminski, Gert Smolka:
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse. 210-225
Description Logics
- Franz Baader, Rafael Peñaloza
Automata-Based Axiom Pinpointing. 226-241 - Boris Motik, Ian Horrocks
Individual Reuse in Description Logic Reasoning. 242-258 - Boris Konev
The Logical Difference Problem for Description Logic Terminologies. 259-274
System Descriptions 2
- Laura Kovács
Aligator: A Mathematica Package for Invariant Generation (System Description). 275-282 - Jens Otten
leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions). 283-291 - Konstantin Korovin:
iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). 292-298 - Rajeev Goré, Linda Postniece:
An Experimental Evaluation of Global Caching for (System Description). 299-305 - Haruhiko Sato, Sarah Winkler
Multi-completion with Termination Tools (System Description). 306-312 - Francisco Durán
MTT: The Maude Termination Tool (System Description). 313-319 - Anders Schack-Nielsen, Carsten Schürmann:
Celf - A Logical Framework for Deductive and Concurrent Systems (System Description). 320-326
Invited Talk
- Nachum Dershowitz:
Canonicity! 327-331
Equational Theories
- Thierry Boy de la Tour, Mnacho Echenim, Paliath Narendran:
Unification and Matching Modulo Leaf-Permutative Equational Presentations. 332-347 - Vincent van Oostrom
Modularity of Confluence. 348-363 - Nao Hirokawa
Automated Complexity Analysis Based on the Dependency Pair Method. 364-379 - Maria Paola Bonacina, Nachum Dershowitz:
Canonical Inference for Implicational Systems. 380-395
Invited Talk
- Hubert Comon-Lundh:
Challenges in the Automated Verification of Security Protocols. 396-409
Theorem Proving 1
- Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. 410-425 - Juan Antonio Navarro Pérez, Andrei Voronkov:
Proof Systems for Effectively Propositional Logic. 426-440 - Josef Urban, Geoff Sutcliffe
MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. 441-456
CASC
- Geoff Sutcliffe
CASC-J4 The 4th IJCAR ATP System Competition. 457-458
Theorem Proving 2
- Arnaud Fietzke, Christoph Weidenbach:
Labelled Splitting. 459-474 - Leonardo Mendonça de Moura, Nikolaj S. Bjørner:
Engineering DPLL(T) + Saturation. 475-490 - Christoph Benzmüller
THF0 - The Core of the TPTP Language for Higher-Order Logic. 491-506
Logical Frameworks
- Vivek Nigam, Dale Miller
Focusing in Linear Meta-logic. 507-522
Tree Automata
- Benoît Boyer, Thomas Genet, Thomas P. Jensen:
Certifying a Tree Automata Completion Checker. 523-538 - Adel Bouhoula, Florent Jacquemard:
Automated Induction with Constrained Tree Automata. 539-554
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-13 18:59 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: