CADE 2003 - PDF Preprint Papers

CADE 2003 Automated Deduction

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CADE-2003 Paper

click to vote

CADE
2003
Springer

188views Logical Reasoning» more CADE 2003»

Algorithms for Ordinal Arithmetic

14 years 11 months ago

Download www.cs.utexas.edu

Ordinals form the basis for termination proofs in ACL2. Currently, ACL2 uses a rather inefficient representation for the ordinals up to 0 and provides limited support for reasoning...

Panagiotis Manolios, Daron Vroon

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	188	Algorithms for Ordinal Arithmetic	claim
2	174	Proving Pointer Programs in Higher-Order Logic	claim
3	172	Certifying Solutions to Permutation Group Problems	claim
4	166	Proof Search and Proof Check for Equational and Inductive Theorems	claim
5	163	adbmal	claim
6	158	A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae	claim
7	152	Automating the Dependency Pair Method	claim
8	140	Optimizing Higher-Order Pattern Unification	claim
9	139	Foundational Certified Code in a Metalogical Framework	claim
10	139	Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms	claim
11	134	The CADE-19 ATP System Competition	claim
12	132	How to Prove Inductive Theorems? QUODLIBET!	claim
13	124	Equational Abstractions	claim
14	123	Canonization for Disjoint Unions of Theories	claim
15	119	Source-Tracking Unification	claim
16	112	The Model Evolution Calculus	claim
17	112	TRP++2.0: A Temporal Resolution Prover	claim
18	112	Subset Types and Partial Functions	claim
19	110	IsaPlanner: A Prototype Proof Planner in Isabelle	claim
20	97	Monodic Temporal Resolution	claim
21	97	Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers