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