CADE 2009 - PDF Preprint Papers

CADE 2009 Automated Deduction

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CADE-2009 Paper

click to vote

CADE
2009
Springer

400views Logical Reasoning» more CADE 2009»

Instantiation-Based Automated Reasoning: From Theory to Practice

14 years 16 days ago

Download www.cs.man.ac.uk

Konstantin Korovin

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	400	Instantiation-Based Automated Reasoning: From Theory to Practice	claim
2	321	Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic	claim
3	218	Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival	claim
4	208	Computing Knowledge in Security Protocols under Convergent Equational Theories	claim
5	200	Progress in the Development of Automated Theorem Proving for Higher-Order Logic	claim
6	197	Beyond Dependency Graphs	claim
7	196	A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs	claim
8	194	Complexity of Fractran and Productivity	claim
9	189	Does This Set of Clauses Overlap with at Least One MUS?	claim
10	189	Interpolant Generation for UTVPI	claim
11	182	Decidability Results for Saturation-Based Model Building	claim
12	180	Termination Analysis by Dependency Pairs and Inductive Theorem Proving	claim
13	178	A Generalization of Semenov's Theorem to Automata over Real Numbers	claim
14	173	Interpolation and Symbol Elimination	claim
15	172	Complexity and Algorithms for Monomial and Clausal Predicate Abstraction	claim
16	168	An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability	claim
17	167	Real World Verification	claim
18	164	Dei: A Theorem Prover for Terms with Integer Exponents	claim
19	163	Ground Interpolation for Combined Theories	claim
20	150	Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method	claim
21	148	A Refined Resolution Calculus for CTL	claim
22	144	SPASS Version 3.5	claim
23	142	veriT: An Open, Trustable and Efficient SMT-Solver	claim
24	135	Superposition and Model Evolution Combined	claim
25	134	A Tableau Calculus for Regular Grammar Logics with Converse	claim
26	121	System Description: H-PILoT	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers