Sciweavers

CADE
2003
Springer
14 years 11 months ago
Automating the Dependency Pair Method
Developing automatable methods for proving termination of term rewrite systems that resist traditional techniques based on simplification orders has become an active research area ...
Nao Hirokawa, Aart Middeldorp
CADE
2003
Springer
14 years 11 months ago
adbmal
We make the notion of scope in the -calculus explicit. To that end, the syntax of the -calculus is extended with an end-of-scope operator , matching the usual opening of a scope du...
Dimitri Hendriks, Vincent van Oostrom
CADE
2003
Springer
14 years 11 months ago
Source-Tracking Unification
We propose a practical path-based framework for deriving and simplifying source-tracking information for term unification in the empty theory. Such a framework is useful for debugg...
Venkatesh Choppella, Christopher T. Haynes
CADE
2003
Springer
14 years 11 months ago
IsaPlanner: A Prototype Proof Planner in Isabelle
IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjectur...
Lucas Dixon, Jacques D. Fleuriot
CADE
2003
Springer
14 years 11 months ago
Proof Search and Proof Check for Equational and Inductive Theorems
This paper presents on-going researches on theoretical and practical issues of combining rewriting based automated theorem proving and user-guided proof development, with the stron...
Eric Deplagne, Claude Kirchner, Hélè...
CADE
2003
Springer
14 years 11 months ago
Monodic Temporal Resolution
Anatoli Degtyarev, Michael Fisher, Boris Konev
CADE
2003
Springer
14 years 11 months ago
Foundational Certified Code in a Metalogical Framework
Foundational certified code systems seek to prove untrusted programs to be safe relative to safety policies given in terms of actual machine architectures, thereby improving the s...
Karl Crary, Susmit Sarkar
CADE
2003
Springer
14 years 11 months ago
Certifying Solutions to Permutation Group Problems
We describe the integration of permutation group algorithms with proof planning. We consider eight basic questions arising in computational permutation group theory, for which our ...
Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Vo...
CADE
2003
Springer
14 years 11 months ago
How to Prove Inductive Theorems? QUODLIBET!
Jürgen Avenhaus, Ulrich Kühler, Tobias S...