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...
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...
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...
Linear arithmetic decision procedures form an important part of theorem provers for program verification. In most verification benchmarks, the linear arithmetic constraints are dom...
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 ...
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...
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...
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...
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 ...
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...