Ulrich Furbach, Natarajan Shankar
Proceedings of the Third International Joint Conference on Automated Reasoning
IJCAR, 2006.

@proceedings{IJCAR-2006,
	address       = "Seattle, Washington, USA",
	editor        = "Ulrich Furbach and Natarajan Shankar",
	isbn          = "3-540-37187-7",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Third International Joint Conference on Automated Reasoning}",
	volume        = 4130,
	year          = 2006,
}

Contents (53 items)

10 ×#logic
7 ×#proving
6 ×#automation
6 ×#higher-order
3 ×#calculus
3 ×#finite
3 ×#reasoning
3 ×#recursion
3 ×#semantics
2 ×#algorithm

IJCAR-2006-Buchberger

Mathematical Theory Exploration (BB), pp. 1–2.

IJCAR-2006-Darwiche #compilation #evolution #satisfiability

Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation (AD), p. 3.

IJCAR-2006-Miller #reasoning #representation #semantics

Representing and Reasoning with Operational Semantics (DM), pp. 4–20.

IJCAR-2006-NipkowBS #graph

Flyspeck I: Tame Graphs (TN, GB, PS), pp. 21–35.

IJCAR-2006-SorgeMMC #automation #invariant #verification

Automatic Construction and Verification of Isotopy Invariants (VS, AM, RLM, SC), pp. 36–51.

IJCAR-2006-Boldo #algorithm #float #proving

Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms (SB), pp. 52–66.

IJCAR-2006-SutcliffeSCG #finite #using

Using the TPTP Language for Writing Derivations and Finite Interpretations (GS, SS, KC, AVG), pp. 67–81.

IJCAR-2006-LevySV #unification

Stratified Context Unification Is NP-Complete (JL, MSS, MV), pp. 82–96.

IJCAR-2006-ChaudhuriPP #logic

A Logical Characterization of Forward and Backward Chaining in the Inverse Method (KC, FP, GP), pp. 97–111.

IJCAR-2006-Paskevich #lazy evaluation

Connection Tableaux with Lazy Paramodulation (AP), pp. 112–124.

IJCAR-2006-BaumgartnerS #bottom-up #generative

Blocking and Other Enhancements for Bottom-Up Model Generation Methods (PB, RAS), pp. 125–139.

IJCAR-2006-ZimmerA #reasoning #semantics #web

The MathServe System for Semantic Web Reasoning Services (JZ, SA), pp. 140–144.

IJCAR-2006-JanicicQ

System Description: GCLCprover + GeoThms (PJ, PQ), pp. 145–150.

IJCAR-2006-HendrixMO #axiom #linear #order #specification

A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms (JH, JM, HO), pp. 151–155.

IJCAR-2006-GelderS #automation #generative #higher-order #logic #parsing

Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation (AVG, GS), pp. 156–161.

IJCAR-2006-ConstableM #proving #semantics #source code

Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics (RLC, WM), pp. 162–176.

IJCAR-2006-Harrison #self #towards

Towards Self-verification of HOL Light (JH), pp. 177–191.

IJCAR-2006-McLaughlin #higher-order

An Interpretation of Isabelle/HOL in HOL Light (SM), pp. 192–204.

IJCAR-2006-Brown #set #type system

Combining Type Theory and Untyped Set Theory (CEB), pp. 205–219.

IJCAR-2006-BenzmullerBK #logic

Cut-Simulation in Impredicative Logics (CB, CEB, MK), pp. 220–234.

IJCAR-2006-Sofronie-Stokkermans

Interpolation in Local Theory Extensions (VSS), pp. 235–250.

IJCAR-2006-ZamanskyA #calculus #canonical #quantifier

Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers (AZ, AA), pp. 251–265.

IJCAR-2006-BeckertP #logic

Dynamic Logic with Non-rigid Functions (BB, AP), pp. 266–280.

IJCAR-2006-GieslST #automation #dependence #framework #proving #termination

Automatic Termination Proofs in the Dependency Pair Framework (JG, PSK, RT), pp. 281–286.

IJCAR-2006-BaaderLS #named #ontology #polynomial

CEL — A Polynomial-Time Reasoner for Life Science Ontologies (FB, CL, BS), pp. 287–291.

IJCAR-2006-TsarkovH #logic

FaCT++ Description Logic Reasoner: System Description (DT, IH), pp. 292–297.

IJCAR-2006-ObuaS #higher-order

Importing HOL into Isabelle/HOL (SO, SS), pp. 298–302.

IJCAR-2006-NivelleM #finite #geometry #proving

Geometric Resolution: A Proof Procedure Based on Finite Model Search (HdN, JM), pp. 303–317.

IJCAR-2006-JiaZ #finite #morphism

A Powerful Technique to Eliminate Isomorphism in Finite Model Search (XJ, JZ), pp. 318–331.

IJCAR-2006-KoprowskiZ #automation #infinity #order #recursion #term rewriting

Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems (AK, HZ), pp. 332–346.

IJCAR-2006-DyckhoffKL #bound #calculus #logic

Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic (RD, DK, SL), pp. 347–361.

IJCAR-2006-Pientka #approach #higher-order #lightweight #unification

Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach (BP), pp. 362–376.

IJCAR-2006-Rabe #dependent type #first-order #logic

First-Order Logic with Dependent Types (FR), pp. 377–391.

IJCAR-2006-KozenKR #automation #category theory #proving

Automating Proofs in Category Theory (DK, CK, ER), pp. 392–407.

IJCAR-2006-Zumkeller #modelling #optimisation

Formal Global Optimisation with Taylor Models (RZ), pp. 408–422.

IJCAR-2006-GregoireT #composition #functional #library #scalability

A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers (BG, LT), pp. 423–437.

IJCAR-2006-Mahboubi #algorithm #implementation #performance #proving

Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials (AM), pp. 438–452.

IJCAR-2006-ReeberH #satisfiability #subclass

A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) (ER, WAHJ), pp. 453–467.

IJCAR-2006-LahiriM #constraints #linear

Solving Sparse Linear Constraints (SKL, MM), pp. 468–482.

IJCAR-2006-GrinchteinLP #automation #invariant #network

Inferring Network Invariants Automatically (OG, ML, NP), pp. 483–497.

IJCAR-2006-UrbanB #combinator #data type #higher-order #recursion

A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (CU, SB), pp. 498–512.

IJCAR-2006-BonacinaGNRZ #decidability

Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures (MPB, SG, EN, SR, DZ), pp. 513–527.

IJCAR-2006-Chaieb #quantifier #verification

Verifying Mixed Real-Integer Quantifier Elimination (AC), pp. 528–540.

IJCAR-2006-DemriL #logic

Presburger Modal Logic Is PSPACE-Complete (SD, DL), pp. 541–556.

IJCAR-2006-JacquemardRV #automaton #constraints #equation #similarity

Tree Automata with Equality Constraints Modulo Equational Theories (FJ, MR, LV), pp. 557–571.

IJCAR-2006-Sutcliffe #contest #named

CASC-J3 — The 3rd IJCAR ATP System Competition (GS), pp. 572–573.

IJCAR-2006-EndrullisWZ #matrix #proving #term rewriting #termination

Matrix Interpretations for Proving Termination of Term Rewriting (JE, JW, HZ), pp. 574–588.

IJCAR-2006-Krauss #higher-order #logic #recursion

Partial Recursive Functions in Higher-Order Logic (AK), pp. 589–603.

IJCAR-2006-Werner #on the

On the Strength of Proof-Irrelevant Type Theories (BW), pp. 604–618.

IJCAR-2006-Walukiewicz-ChrzaszczC #calculus #consistency

Consistency and Completeness of Rewriting in the Calculus of Constructions (DWC, JC), pp. 619–631.

IJCAR-2006-DoughertyFK #policy #reasoning #specification

Specifying and Reasoning About Dynamic Access-Control Policies (DJD, KF, SK), pp. 632–646.

IJCAR-2006-TomanW #dependence #functional #logic #on the

On Keys and Functional Dependencies as First-Class Citizens in Description Logics (DT, GEW), pp. 647–661.

IJCAR-2006-KazakovM

A Resolution-Based Decision Procedure for SHOIQ (YK, BM), pp. 662–677.