Skip to content

Automated Reasoning Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings

Spend $50 to get a free movie!

ISBN-10: 3540371877

ISBN-13: 9783540371878

Edition: 2006

Authors: Ulrich Furbach, Natarajan Shankar

List price: $109.99
Blue ribbon 30 day, 100% satisfaction guarantee!
Out of stock
what's this?
Rush Rewards U
Members Receive:
Carrot Coin icon
XP icon
You have reached 400 XP and carrot coins. That is the daily max!


This book constitutes the refereed proceedings of the Third International Joint Conference on Automated Reasoning, IJCAR 2006, held in Seattle, WA, USA in August 2006 as part of the 4th Federated Logic Conference, FLoC 2006. IJCAR 2006 is a merger of CADE, FroCoS, FTP, TABLEAUX, and TPHOLs. The 41 revised full research papers and 8 revised system descriptions presented together with 3 invited papers and a summary of a systems competition were carefully reviewed and selected from a total of 152 submissions. The papers address the entire spectrum of research in automated reasoning including formalization of mathematics, proof theory, proof search, description logics, interactive proof…    
Customers also bought

Book details

List price: $109.99
Copyright year: 2006
Publisher: Springer Berlin / Heidelberg
Publication date: 8/3/2006
Binding: Paperback
Pages: 688
Size: 5.98" wide x 9.02" long x 1.00" tall
Weight: 4.708
Language: English

Mathematical theory exploration
Searching while keeping a trace : the evolution from satisfiability to knowledge compilation
Representing and reasoning with operational semantics
Flyspeck I : tame graphs
Automatic construction and verification of isotopy invariants
Pitfalls of a full floating-point proof : example on the formal proof of the Veltkamp/Dekker algorithms
Using the TPTP language for writing derivations and finite interpretations
Stratified context unification is NP-complete
A logical characterization of forward and backward chaining in the inverse method
Connection tableaux with lazy paramodulation
Blocking and other enhancements for bottom-up model generation methods
The MathServe system for semantic Web reasoning services
System description : GCLCprover + GeoThms
A sufficient completeness checker for linear order-sorted specifications Modulo Axioms
Extending the TPTP language to higher-order logic with automated parser generation
Extracting programs from constructive HOL proofs via IZF set-theoretic semantics
Towards self-verification of HOL light
An interpretation of Isabelle/HOL in HOL light
Combining type theory and untyped set theory
Cut-simulation in impredicative logics
Interpolation in local theory extensions
Canonical Gentzcn-type Calculi with (n,k)-ary quantifiers
Dynamic logic with non-rigid functions
AProVE 1.2 : automatic termination proofs in the dependency pair framework
CEL - a polynomial-time reasoner for life science ontologies
FaCT++ description logic reasoner : system description
Importing HOL into Isabelle/HOL
Geometric resolution : a proof procedure based on finite model search
A powerful technique to eliminate isomorphism in finite model search
Automation of recursive path ordering for infinite labelled rewrite systems
Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic
Eliminating redundancy in higher-order unification : a lightweight approach
First-order logic with dependent types
Automating proofs in category theory
Formal global optimisation with taylor models
A purely functional library for modular arithmetic and its application to certifying large prime numbers
Proving formally the implementation of an efficient gcd algorithm for polynomials
A SAT-based decision procedure for the subclass of unrollable list formulas in ACL2 (SULFA)
Solving sparse linear constraints
Inferring network invariants automatically
A recursion combinator for nominal datatypes implemented in Isabelle/HOL
Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures
Verifying mixed real-integer quantifier elimination
Presburger modal logic is PSPACE-complete
Tree automata with equality constraints modulo equational theories
CASC-J3 - the 3rd IJCAR ATP system competition
Matrix interpretations for proving termination of term rewriting
Partial recursive functions in higher-order logic
On the strength of proof-irrelevant type theories
Consistency and completeness of rewriting in the calculus of constructions
Specifying and reasoning about dynamic access-control policies
On keys and functional dependencies as first-class citizens in description logics
A resolution-based decision procedure for SHOIQ