CADE 2005 - PDF Preprint Papers

CADE 2005 Automated Deduction

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CADE-2005 Paper

click to vote

CADE
2005
Springer

198views Logical Reasoning» more CADE 2005»

A Proof-Producing Decision Procedure for Real Arithmetic

14 years 4 months ago

Download www.cl.cam.ac.uk

We present a fully proof-producing implementation of a quantifier elimination procedure for real closed fields. To our knowledge, this is the first generally useful proof-producing...

Sean McLaughlin, John Harrison

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	198	A Proof-Producing Decision Procedure for Real Arithmetic	claim
2	195	An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic	claim
3	165	Tabling for Higher-Order Logic Programming	claim
4	163	A Combination Method for Generating Interpolants	claim
5	150	The Decidability of the First-Order Theory of Knuth-Bendix Order	claim
6	147	Privacy-Sensitive Information Flow with JML	claim
7	143	Reflecting Proofs in First-Order Logic with Equality	claim
8	140	Deciding Monodic Fragments by Temporal Resolution	claim
9	137	Connecting Many-Sorted Theories	claim
10	132	The OWL Instance Store: System Description	claim
11	132	Regular Protocols and Attacks with Regular Knowledge	claim
12	132	KRHyper - In Your Pocket	claim
13	126	Hierarchic Reasoning in Local Theory Extensions	claim
14	123	Temporal Logics over Transitive States	claim
15	121	A Focusing Inverse Method Theorem Prover for First-Order Linear Logic	claim
16	119	Nominal Techniques in Isabelle/HOL	claim
17	118	Well-Nested Context Unification	claim
18	117	Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures	claim
19	113	The Model Evolution Calculus with Equality	claim
20	111	Proof Planning for First-Order Temporal Logic	claim
21	106	Deduction with XOR Constraints in Security API Modelling	claim
22	104	Reasoning in Extensional Type Theory with Equality	claim
23	102	System Description: Multi A Multi-strategy Proof Planner	claim
24	101	The MathSAT 3 System	claim
25	100	On the Complexity of Equational Horn Clauses	claim
26	97	sKizzo: A Suite to Evaluate and Certify QBFs	claim
27	96	The CoRe Calculus	claim
28	86	Proving Properties of Incremental Merkle Trees	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers