default search action
3rd IJCAR 2006: Seattle, WA, USA
- Ulrich Furbach, Natarajan Shankar:
Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. Lecture Notes in Computer Science 4130, Springer 2006, ISBN 3-540-37187-7
Invited Talks
- Bruno Buchberger:
Mathematical Theory Exploration. 1-2 - Adnan Darwiche:
Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation. 3 - Dale Miller
:
Representing and Reasoning with Operational Semantics. 4-20
Proofs
- Tobias Nipkow, Gertrud Bauer, Paula Schultz:
Flyspeck I: Tame Graphs. 21-35 - Volker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton:
Automatic Construction and Verification of Isotopy Invariants. 36-51 - Sylvie Boldo:
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. 52-66 - Geoff Sutcliffe
Using the TPTP Language for Writing Derivations and Finite Interpretations. 67-81
Search
- Jordi Levy
Stratified Context Unification Is NP-Complete. 82-96 - Kaustuv Chaudhuri, Frank Pfenning, Greg Price:
A Logical Characterization of Forward and Backward Chaining in the Inverse Method. 97-111 - Andrey Paskevich:
Connection Tableaux with Lazy Paramodulation. 112-124 - Peter Baumgartner, Renate A. Schmidt:
Blocking and Other Enhancements for Bottom-Up Model Generation Methods. 125-139
System Description 1
- Jürgen Zimmer, Serge Autexier
The MathServe System for Semantic Web Reasoning Services. 140-144 - Predrag Janicic, Pedro Quaresma
System Description: GCLCprover + GeoThms. 145-150 - Joe Hendrix, José Meseguer, Hitoshi Ohsaki:
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. 151-155 - Allen Van Gelder, Geoff Sutcliffe
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. 156-161
Higher-Order Logic
- Robert L. Constable, Wojciech Moczydlowski:
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics. 162-176 - John Harrison:
Towards Self-verification of HOL Light. 177-191 - Sean McLaughlin:
An Interpretation of Isabelle/HOL in HOL Light. 192-204 - Chad E. Brown:
Combining Type Theory and Untyped Set Theory. 205-219
Proof Theory
- Christoph Benzmüller, Chad E. Brown, Michael Kohlhase:
Cut-Simulation in Impredicative Logics. 220-234 - Viorica Sofronie-Stokkermans:
Interpolation in Local Theory Extensions. 235-250 - Anna Zamansky, Arnon Avron:
Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers. 251-265 - Bernhard Beckert, André Platzer:
Dynamic Logic with Non-rigid Functions. 266-280
System Description 2
- Jürgen Giesl
Automatic Termination Proofs in the Dependency Pair Framework. 281-286 - Franz Baader, Carsten Lutz, Boontawee Suntisrivaraporn:
CEL - A Polynomial-Time Reasoner for Life Science Ontologies. 287-291 - Dmitry Tsarkov, Ian Horrocks:
FaCT++ Description Logic Reasoner: System Description. 292-297 - Steven Obua, Sebastian Skalberg:
Importing HOL into Isabelle/HOL. 298-302
Search
- Hans de Nivelle, Jia Meng:
Geometric Resolution: A Proof Procedure Based on Finite Model Search. 303-317 - Xiangxue Jia, Jian Zhang:
A Powerful Technique to Eliminate Isomorphism in Finite Model Search. 318-331 - Adam Koprowski, Hans Zantema:
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems. 332-346
Proof Theory
- Roy Dyckhoff, Delia Kesner, Stéphane Lengrand:
Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic. 347-361 - Brigitte Pientka:
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. 362-376 - Florian Rabe:
First-Order Logic with Dependent Types. 377-391
Proof Checking
- Dexter Kozen, Christoph Kreitz, Eva Richter:
Automating Proofs in Category Theory. 392-407 - Roland Zumkeller:
Formal Global Optimisation with Taylor Models. 408-422 - Benjamin Grégoire, Laurent Théry:
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. 423-437 - Assia Mahboubi:
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. 438-452
Combination
- Erik Reeber, Warren A. Hunt Jr.:
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). 453-467 - Shuvendu K. Lahiri, Madanlal Musuvathi:
Solving Sparse Linear Constraints. 468-482 - Olga Grinchtein, Martin Leucker
Inferring Network Invariants Automatically. 483-497 - Christian Urban, Stefan Berghofer:
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. 498-512
Decision Procedures
- Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. 513-527 - Amine Chaieb:
Verifying Mixed Real-Integer Quantifier Elimination. 528-540 - Stéphane Demri, Denis Lugiez:
Presburger Modal Logic Is PSPACE-Complete. 541-556 - Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron:
Tree Automata with Equality Constraints Modulo Equational Theories. 557-571
CASC-J3
- Geoff Sutcliffe
CASC-J3 - The 3rd IJCAR ATP System Competition. 572-573
Rewriting
- Jörg Endrullis
Matrix Interpretations for Proving Termination of Term Rewriting. 574-588 - Alexander Krauss:
Partial Recursive Functions in Higher-Order Logic. 589-603 - Benjamin Werner:
On the Strength of Proof-Irrelevant Type Theories. 604-618 - Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz:
Consistency and Completeness of Rewriting in the Calculus of Constructions. 619-631
Description Logic
- Daniel J. Dougherty, Kathi Fisler
Specifying and Reasoning About Dynamic Access-Control Policies. 632-646 - David Toman, Grant E. Weddell:
On Keys and Functional Dependencies as First-Class Citizens in Description Logics. 647-661 - Yevgeny Kazakov, Boris Motik:
A Resolution-Based Decision Procedure for SHOIQ. 662-677
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-16 22:15 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: