Disunification is the problem of deciding satisfiability of a system of equations and disequations w.r.t. a given equational theory. In this paper we study the disunification problem in the context of ACI1 equational theories. We provide a …
We present a Natural Deduction proof system for the pro- positional modal μ-calculus, and its formalization in the Calculus of In- ductive Constructions. We address several problematic issues, such as the use of higher-order abstract syntax in …
We review and compare the main techniques considered to represent finite sets in logic languages. We present a technique that combines the benefits of the previous techniques, avoiding their drawbacks. We show how to verify satisfiability of any …
T-resolution parametrically generalizes standard resolution with respect to a first-order theory T (the parameter). The inherent power of its derivation rule, however, makes it difficult to develop efficient unrestricted T -resolution based systems. …
Natural Deduction style presentations of program logics are useful in view of the implementation of such logics in interactive proof development environments, based on type theory, such as LEGO, Coq, etc. In fact, ND-style systems are the kind of …
The first order theories of lists, bags, compact-lists (i.e., lists where the number of contiguous occurrences of each element is immaterial), and sets are introduced via axioms. Such axiomatizations are shown to be espe- cially suitable for the …