Sciweavers

CADE
2006
Springer
15 years 22 days ago
An Interpretation of Isabelle/HOL in HOL Light
We define an interpretation of the Isabelle/HOL logic in HOL Light and its metalanguage, OCaml. Some aspects of the Isabelle logic are not representable directly in the HOL Light o...
Sean McLaughlin
CADE
2006
Springer
15 years 22 days ago
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correctness of our implementation of the subresulta...
Assia Mahboubi
CADE
2006
Springer
15 years 22 days ago
Stratified Context Unification Is NP-Complete
Context Unification is the problem to decide for a given set of second-order equations E where all second-order variables are unary, whether there exists a unifier, such that for e...
Jordi Levy, Manfred Schmidt-Schauß, Mateu Vi...
CADE
2006
Springer
15 years 22 days ago
Solving Sparse Linear Constraints
Linear arithmetic decision procedures form an important part of theorem provers for program verification. In most verification benchmarks, the linear arithmetic constraints are dom...
Shuvendu K. Lahiri, Madanlal Musuvathi
CADE
2006
Springer
15 years 22 days ago
Partial Recursive Functions in Higher-Order Logic
Abstract. Based on inductive definitions, we develop an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for ...
Alexander Krauss
CADE
2006
Springer
15 years 22 days ago
Automating Proofs in Category Theory
Abstract. We introduce a semi-automated proof system for basic category-theoretic reasoning. It is based on a first-order sequent calculus that captures the basic properties of cat...
Dexter Kozen, Christoph Kreitz, Eva Richter
CADE
2006
Springer
15 years 22 days ago
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
Abstract. Semantic labelling is a transformational technique for proving termination of Term Rewriting Systems (TRSs). Only its variant with finite sets of labels was used so far i...
Adam Koprowski, Hans Zantema
CADE
2006
Springer
15 years 22 days ago
A Resolution-Based Decision Procedure for SHOIQ
We present a resolution-based decision procedure for the description logic SHOIQ--the logic underlying the Semantic Web ontology language OWL-DL. Our procedure is goal-oriented, an...
Yevgeny Kazakov, Boris Motik
CADE
2006
Springer
15 years 22 days ago
Tree Automata with Equality Constraints Modulo Equational Theories
This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential ...
Florent Jacquemard, Laurent Vigneron, Michaël...
CADE
2006
Springer
15 years 22 days ago
Inferring Network Invariants Automatically
Abstract. Verification by network invariants is a heuristic to solve uniform verification of parameterized systems. Given a system P, a network invariant for P is that abstracts th...
Olga Grinchtein, Martin Leucker, Nir Piterman