CADE 2006 - PDF Preprint Papers

CADE 2006 Automated Deduction

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CADE-2006 Paper

click to vote

CADE
2006
Springer

192views Logical Reasoning» more CADE 2006»

Formal Global Optimisation with Taylor Models

14 years 5 months ago

Download www.nianet.org

Roland Zumkeller

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	192	Formal Global Optimisation with Taylor Models	claim
2	188	CEL - A Polynomial-Time Reasoner for Life Science Ontologies	claim
3	176	Description Logic Reasoner: System Description	claim
4	172	Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics	claim
5	164	The MathServe System for Semantic Web Reasoning Services	claim
6	163	Automatic Termination Proofs in the Dependency Pair Framework	claim
7	162	Blocking and Other Enhancements for Bottom-Up Model Generation Methods	claim
8	162	Cut-Simulation in Impredicative Logics	claim
9	156	Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures	claim
10	151	Combining Type Theory and Untyped Set Theory	claim
11	150	On the Strength of Proof-Irrelevant Type Theories	claim
12	147	Partial Recursive Functions in Higher-Order Logic	claim
13	139	Inferring Network Invariants Automatically	claim
14	137	Dynamic Logic with Non-rigid Functions	claim
15	134	Automatic Construction and Verification of Isotopy Invariants	claim
16	134	A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms	claim
17	134	Interpolation in Local Theory Extensions	claim
18	132	Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach	claim
19	129	Importing HOL into Isabelle/HOL	claim
20	128	Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems	claim
21	127	Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic	claim
22	127	Matrix Interpretations for Proving Termination of Term Rewriting	claim
23	126	System Description: GCLCprover + GeoThms	claim
24	125	Using the TPTP Language for Writing Derivations and Finite Interpretations	claim
25	124	Verifying Mixed Real-Integer Quantifier Elimination	claim
26	124	Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers	claim
27	120	An Interpretation of Isabelle/HOL in HOL Light	claim
28	118	Tree Automata with Equality Constraints Modulo Equational Theories	claim
29	117	Stratified Context Unification Is NP-Complete	claim
30	117	Representing and Reasoning with Operational Semantics	claim
31	115	Solving Sparse Linear Constraints	claim
32	114	A Resolution-Based Decision Procedure for SHOIQ	claim
33	112	Automating Proofs in Category Theory	claim
34	111	Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation	claim
35	109	Towards Self-verification of HOL Light	claim
36	108	Geometric Resolution: A Proof Procedure Based on Finite Model Search	claim
37	106	On Keys and Functional Dependencies as First-Class Citizens in Description Logics	claim
38	105	A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL	claim
39	105	Presburger Modal Logic Is PSPACE-Complete	claim
40	102	Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials	claim
41	101	Specifying and Reasoning About Dynamic Access-Control Policies	claim
42	97	Connection Tableaux with Lazy Paramodulation	claim
43	84	A Logical Characterization of Forward and Backward Chaining in the Inverse Method	claim
44	79	Flyspeck I: Tame Graphs	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers