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

152views Logical Reasoning» more CADE 2009»

Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic

2 years 2 months ago

Download www.lsi.upc.edu

Abstract. Polynomial constraint-solving plays a prominent role in several areas of engineering and software verification. In particular, polynomial constraint solving has a long an...

Albert Rubio, Cristina Borralleras, Enric Rodr&iac...

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	152	Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic	claim
2	118	Instantiation-Based Automated Reasoning: From Theory to Practice	claim
3	84	Does This Set of Clauses Overlap with at Least One MUS?	claim
4	76	Complexity of Fractran and Productivity	claim
5	68	Beyond Dependency Graphs	claim
6	65	Interpolation and Symbol Elimination	claim
7	64	Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival	claim
8	63	Progress in the Development of Automated Theorem Proving for Higher-Order Logic	claim
9	62	Dei: A Theorem Prover for Terms with Integer Exponents	claim
10	60	A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs	claim
11	59	A Refined Resolution Calculus for CTL	claim
12	58	Interpolant Generation for UTVPI	claim
13	54	Complexity and Algorithms for Monomial and Clausal Predicate Abstraction	claim
14	54	Decidability Results for Saturation-Based Model Building	claim
15	53	Computing Knowledge in Security Protocols under Convergent Equational Theories	claim
16	51	veriT: An Open, Trustable and Efficient SMT-Solver	claim
17	51	Real World Verification	claim
18	48	An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability	claim
19	44	Superposition and Model Evolution Combined	claim
20	44	SPASS Version 3.5	claim
21	44	System Description: H-PILoT	claim
22	44	A Tableau Calculus for Regular Grammar Logics with Converse	claim
23	44	Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method	claim
24	41	Ground Interpolation for Combined Theories	claim
25	39	Termination Analysis by Dependency Pairs and Inductive Theorem Proving	claim
26	37	A Generalization of Semenov's Theorem to Automata over Real Numbers	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers