Overview

Theses

Papers

Reasoning in/about complex systems Hierarchical reasoning: Implementation

Hierarchical and modular reasoning in combinations of theories

Applications of hierarchical reasoning to verification

Models for interacting systems

Automated theorem proving in lattice-ordered algebraic structures

Boolean equations

Priestley duality for distributive lattices with operators

Automated theorem proving in varieties of distributive lattices with operators

Algebraic structures related to non-classical logics

Automated theorem proving in non-classical logics

Finitely-valued logics

More general logics

Unification

Automated Theorem Proving. The Knuth-Bendix algorithm and some extensions

Diploma Thesis, University Bucharest, 1987; Abstract, BibTex-Entry.

Modal Algebras and Rewriting Algorithms

Specialization Thesis, University Bucharest, 1988; Abstract, BibTex-Entry.

Fibered Structures and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems

PhD Thesis, RISC Linz, Johannes Kepler University, Linz, Austria, 1997; Abstract

Download: PostScript, BibTex-Entry.

For a short description of an implementation of local/hierarchical reasoning and various tests on problems from verification follow this link (ongoing joint work with Carsten Ihlemann and Swen Jacobs)

System description H-PILoT

Carsten Ihlemann and Viorica Sofronie-Stokkermans
In: Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction, 131-139

Abstract: H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions) is a program for hierarchical reasoning in extensions of logical theories with additional functions axiomatized by a set of (universally quantified) clauses: deduction problems in the theory extension are reduced to deduction problems in the base theory. Specialized provers, as well as standard SMT solvers, are then used for testing the satisfiability of the formulae obtained after the reduction. The hierarchical reduction used in H-PILoT is always sound; it is complete for the class of so-called local extensions of a base theory. If the clauses obtained by this reduction belong to a fragment decidable in the base theory, H-PILoT provides a decision procedure for testing satisfiability of ground formulae w.r.t.\ a theory extension, and can also be used for model generation. This is the major advantage of H-PILoT compared with other state-of-the art SMT solvers. H-PILoT can alternatively be used as a tool for ``steering'' the instantiation mechanism of standard SMT provers, in order to provide decision procedures in the case of local theory extensions. This system description provides an overview of H-PILoT and illustrates on some examples the main advantage of using H-PILoT for satisfiability checking in local extensions, in comparison with the performance of general state of the art SMT-provers.

System description H-PILoT Version 1.9

Carsten Ihlemann and Viorica Sofronie-Stokkermans
Extended version of the CADE paper. AVACS Technical Report ATR 61, SFB/TR 14 AVACS, 2010. ISSN: 1860-9821, http://www.avacs.org. Download (.pdf)

On hierarchical reasoning in combinations of theories

Carsten Ihlemann and Viorica Sofronie-Stokkermans
Proceedings of IJCAR 2010. LNAI 6173, pages 30-45.

Abstract: In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense have also a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.

An extended version of this paper appeared as AVACS Technical Report ATR 60, SFB/TR 14 AVACS, 2010. ISSN: 1860-9821, http://www.avacs.org. Download (.pdf)

Hierarchical reasoning for the verification of parametric systems

Proceedings of IJCAR 2010. LNAI 6173, pages 171-187.

Abstract: We study certain classes of verification problems for parametric reactive and hybrid systems, and identify the types of logical theories which can be used for modeling such systems and the reasoning tasks which need to be solved in this context. We identify properties of the underlying theories which ensure that these classes of verification problems can be solved efficiently, give examples of theories with the desired properties, and illustrate the methods we use on several examples.

Locality results for certain extensions of theories with bridging functions

Proceedings CADE 22, LNAI 5663, pages 6783, Springer 2009.

Abstract: In this paper we study possibilities of reasoning about functions over theories of data types which satisfy certain recursion (or homomorphism) properties, with a focus on emphasizing possibilities of hierarchical and modular reasoning in such extensions and combinations thereof. We start by considering theories of absolutely free data structures, and continue by studying extensions of such theories with selectors, with functions which attach scalar data to the data structures and with additional functions defined using a certain type of recursion axioms (possibly having values in a different -- e.g.\ numeric -- domain). We show that in these cases locality results can be established. This allows us to reduce the task of reasoning about the class of recursive functions we consider to reasoning in the underlying theory of absolutely free data structures (resp. in a combination of the theory of absolutely free data structures with the theory attached with the domains of the additional functions). We then show that similar results can be obtained if we relax some assumptions about the absolute freeness of the underlying theory of data types. We investigate the applications of these ideas in verification and cryptography.

Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms

Dagstuhl Seminar Proceedings Vol.09411 "Interaction versus Automation: The two Faces of Deduction", Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2010.

Abstract:We study possibilities of reasoning about \ extensions of base theories with functions which satisfy certain recursion and homomorphism properties. Our focus is on emphasizing possibilities of hierarchical and modular reasoning in such extensions and combinations thereof.

We show that the theory of absolutely free constructors is local, and locality is preserved also in the presence of selectors. These results are consistent with existing decision procedures for this theory (e.g. by Oppen).

We show that, under certain assumptions, extensions of the theory of absolutely free constructors with functions satisfying a certain type of recursion axioms satisfy locality properties, and show that for functions with values in an ordered domain we can combine recursive definitions with boundedness axioms without sacrificing locality. We also address the problem of only considering models whose data part is the {em initial} term algebra of such theories.

We analyze conditions which ensure that similar results can be obtained if we relax some assumptions about the absolute freeness of the underlying theory of data types, and illustrate the ideas on an example from cryptography.

The locality results we establish allow us to reduce the task of reasoning about the class of recursive functions we consider to reasoning in the underlying theory of data structures (possibly combined with the theories associated with the co-domains of the recursive functions). As a by-product, the methods we use provide a possibility of presenting in a different light (and in a different form) locality phenomena studied in cryp-to-gra-phy; we believe that they will allow to better separate rewriting from proving, and thus to give simpler proofs.

Constraint Solving for Interpolation

Andrey Rybalchenko and Viorica Sofronie-Stokkermans
Journal of Symbolic Computation. To appear.

A preliminary version appeared as AVACS Technical Report ATR 56, SFB/TR 14 AVACS, 2009.

Abstract: Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing separation between the sets of `good' and `bad' states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.

Constraint Solving for Interpolation

Andrey Rybalchenko and Viorica Sofronie-Stokkermans
Proceedings VMCAI 2007, LNCS 4349, pages 346-362

Abstract: Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing separation between the sets of `good' and `bad' states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.

Interpolation in local theory extensions

Logical methods in computer science. (Special issue dedicated to IJCAR 2006), To appear.

Abstract: Many problems in mathematics and computer science (e.g. in verification, or when reasoning in and about distributed databases) can be reduced to proving the satisfiability of conjunctions of (ground) literals modulo a background theory. This theory can, for instance, be the extension of a base theory with additional functions or a combination of theories. It is therefore very important to find efficient methods for checking the unsatisfiability of ground formulae in such complex theories. However, it is often equally important to find local causes for inconsistency. Such information is usually provided by interpolants. In this paper we study interpolation in local extensions of a base theory T₀. In such extensions efficient hierarchical reasoning -- in which a prover for the base theory is used as a black box -- is possible. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in T₀ as `black-boxes' in order to generate interpolants in the extension. We provide several examples of such theories, and discuss their applications in verification or knowledge representation.

Download PostScript, PDF

Efficient hierarchical reasoning about functions over numerical domains

KI 2008: Advances in Artificial Intelligence, LNAI 5243, pages 135-143.

Abstract: We show that many properties studied in mathematical analysis (e.g.\ monotonicity, boundedness, inverse or Lipschitz properties, possibly combined with continuity and/or derivability) are expressible as axioms in a class for which sound and complete hierarchical proof methods for testing satisfiability of ground formulae exist. The results are useful for automated reasoning in analysis, and in the verification of hybrid systems.

Download Extended version(.pdf)

Locality and subsumption testing in EL and some of its extensions

Proceedings of AiML 2008. To appear.

Extends the following paper: "Locality and subsumption testing in EL and some of its extensions " Proceedings of the 21st International Workshop on Description Logics (DL2008). CEUR Workshop Proceedings series. Download(.pdf)

Abstract: In this paper we show that subsumption problems in many lightweight description logics (including ${\cal EL}$) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras to obtain uniform PTIME decision procedures for CBox subsumption in ${\cal EL}$ and extensions thereof. These locality considerations allow us to present a new family of logics which extend ${\cal EL}$ with $n$-ary roles and numerical domains and also a new extension of ${\cal EL}^+$.

Download Preprint(.pdf).

Hierarchical and modular reasoning in complex theories: The case of local theory extensions

Proceedings of FroCos 2007 (invited paper for invited talk at joint session of FroCos 2007 and FTP 2007).

Abstract:Many problems in computer science can be reduced to proving the satisfiability of conjunctions of literals w.r.t. a background theory. This theory can be a concrete theory (e.g. the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories. We here give an overview of results on hierarchical and modular reasoning in complex theories. We show that for a special type of extensions of a base theory, which we call local, hierarchic reasoning is possible (i.e. proof tasks in the extension can be hierarchically reduced to proof tasks w.r.t. the base theory). Many theories important for computer science or mathematics fall into this class (typical examples are theories of data structures, theories of free or monotone functions, but also functions occurring in mathematical analysis). In fact, it is often necessary to consider complex extensions, in which various types of functions or data structures need to be taken into account at the same time. We show how such local theory extensions can be identified and under which conditions locality is preserved when combining theories, and we investigate possibilities of efficient modular reasoning in such theory combinations. We present several examples of application domains where such theories occur in a natural way. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of locality.

Download Download(.pdf)

Hierarchical and modular reasoning in complex theories: The case of local theory extensions

Proceedings of FTP 2007 (invited paper for invited talk at joint session of FroCos 2007 and FTP 2007).

Abstract: Many problems in computer science can be reduced to proving the satisfiability of conjunctions of literals w.r.t.\ a background theory. This theory can be a concrete theory (e.g.\ the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories. We here give an overview of results on hierarchical and modular reasoning in complex theories. We show that for a special type of extensions of a base theory, which we call {\em local}, hierarchic reasoning is possible (i.e.\ proof tasks in the extension can be hierarchically reduced to proof tasks w.r.t. the base theory). Many theories important for computer science or mathematics fall into this class (typical examples are theories of data structures, theories of free or monotone functions, but also functions occurring in mathematical analysis). In fact, it is often necessary to consider complex extensions, in which various types of functions or data structures need to be taken into account at the same time. We show how such local theory extensions can be identified and under which conditions locality is preserved when combining theories, and we investigate possibilities of efficient modular reasoning in such theory combinations. We present several examples of application domains where such theories occur in a natural way. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of locality.

Interpolation in local theory extensions

Proceedings of IJCAR 2006, Seattle, USA, LNAI 4130, pages 235-250,Springer, 2006.

Abstract: Many problems in mathematics and computer science (e.g. in verification, or when reasoning in and about distributed databases) can be reduced to proving the satisfiability of conjunctions of (ground) literals modulo a background theory. This theory can, for instance, be the extension of a base theory with additional functions or a combination of theories. It is therefore very important to find efficient methods for checking the unsatisfiability of ground formulae in such complex theories. However, it is often equally important to find local causes for inconsistency. Such information is usually provided by interpolants. In this paper we study interpolation in local extensions of a base theory T₀. In such extensions efficient hierarchical reasoning -- in which a prover for the base theory is used as a black box -- is possible. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in T₀ as `black-boxes' in order to generate interpolants in the extension. We provide several examples of such theories, and discuss their applications in verification or knowledge representation.

Download PostScript, PDF

Hierarchic reasoning in local theory extensions

Proceedings of the 20th International Conference on Automated Deduction (CADE 2005). (Eds.) R. Nieuwenhuis, LNAI 3632, pages 219-234, Springer Verlag, 2005.

Abstract: We show that for special types of extensions of a base theory, which we call local, efficient hierarchic reasoning is possible. We identify situations in which it is possible, for an extension ${\cal T}_1$ of a theory ${\cal T}_0$, to express the decidability and complexity of the universal theory of ${\cal T}_1$ in terms of the decidability resp. complexity of suitable fragments of the theory ${\cal T}_0$ (universal or $\forall \exists$). These results apply to theories related to data types, but also to certain theories of functions from mathematics.

Download PostScript, BibTex-Entry.

Modular Proof Systems for Partial Functions with Evans Equality

(with Harald Ganzinger and Uwe Waldmann)

Information and Computation 204 (10): 1453-1492, 2006.

Abstract: The paper presents a modular superposition calculus for the combination of first-order theories involving both total and partial functions. Modularity means that inferences are pure, only involving clauses over the alphabet of either one, but not both, of the theories. The calculus is shown to be complete provided that functions that are not in the intersection of the component signatures are declared as partial. This result also means that if the unsatisfiability of a goal modulo the combined theory does not depend on the totality of the functions in the extensions, the inconsistency will be effectively found. Moreover, we consider a constraint superposition calculus for the case of hierarchical theories and show that it has a related modularity property. Finally we identify cases where the partial models can always be made total so that modular superposition is also complete with respect to the standard (total function) semantics of the theories.

Download Postscript (gzipped)

Modular Proof Systems for Partial Functions with Weak Equality

(with Harald Ganzinger and Uwe Waldmann)

Proceedings of IJCAR'2004, LNAI 3097, (Eds.) D. Basin, M. Rusinowitch, pages 168-182, Springer Verlag, 2004.

Abstract: The paper presents a modular superposition calculus for the combination of first-order theories involving both total and partial functions. Modularity means that inferences are pure, only involving clauses over the alphabet of either one, but not both, of the theories. The calculus is shown to be complete provided that functions that are not in the intersection of the component signatures are declared as partial. This result also means that if the unsatisfiability of a goal modulo the combined theory does not depend on the totality of the functions in the extensions, the inconsistency will be effectively found. Moreover, we consider a constraint superposition calculus for the case of hierarchical theories and show that it has a related modularity property. Finally we identify cases where the partial models can always be made total so that modular superposition is also complete with respect to the standard (total function) semantics of the theories.

Download PartialFun-bibl.html

Automatic Verification of Parametric Specifications with Complex Topologies

(with Johannes Faber, Carsten Ihlemann and Swen Jacobs)

Proceedings of IFM 2010, to appear.

Abstract: he focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally.

For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations.

At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking.

At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact.

We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.

On local reasoning in verification

(with Carsten Ihlemann and Swen Jacobs)

Proceedings of TACAS'08, LNCS 4963, pages 265-281, Springer 2008.

Abstract: We present a general framework which allows to identify complex theories important in verification for which efficient (hierarchical and modular) reasoning methods exist. The framework we present is based on a general notion of locality. We show that locality considerations allow us to obtain parameterized decidability and complexity results for many (combinations of) theories important in verification in general and in the verification of parametric systems in particular. We give numerous examples of local theory extensions; in particular we show that several theories of data structures studied in the verification literature are local extensions of a base theory. The general framework we use allows us to identify situations in which some of the syntactical restrictions imposed in previous papers can be relaxed.

Download PostScript, PDF

Extends the following paper:

Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs,
" Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
" In Deduction and Decision Procedures, Dagstuhl Seminar Proceedings, F. Baader, B. Cook, J. Giesl, R. Nieuwenhuis (Eds.) IBFI, Schloss Dagstuhl, Germany, December 2007. Download

Verifying CSP-OZ-DC specifications with complex data types and timing parameters

(with Johannes Faber and Swen Jacobs)

Proceedings of IFM 2007: Integrated Formal Methods, LNCS 4591, pages 233-252, Springer, 2007.

Abstract: We extend existing verification methods for CSP-OZ-DC to reason about real-time systems with complex data types and timing parameters. We show that important properties of systems can be encoded in well-behaved logical theories in which hierarchical reasoning is possible. Thus, testing invariants and bounded model checking can be reduced to checking satisfiability of ground formulae over a simple base theory. We illustrate the ideas by means of a simplified version of a case study from the European Train Control System.

Download PostScript, PDF

Constraint Solving for Interpolation

(with Andrey Rybalchenko)

VMCAI'2007: Verification, Model Checking, and Abstract Interpretation, LNCS 4349, pages 346-362. 2007.

Abstract: Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing separation between the sets of `good' and `bad' states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.

Download PDF

Applications of hierarchical reasoning in the verification of complex systems

(with Swen Jacobs)

Electronic Notes in Theoretical Computer Sciences 174/8 (Special issue dedicated to PDPAR'06), pages 39-54, 2007.

Abstract: In this paper we show how hierarchical reasoning can be used to verify properties of complex systems. Chains of local theory extensions are used to model a case study taken from the European Train Control System (ETCS) standard, but considerably simplified. We show how testing invariants and bounded model checking can automatically be reduced to checking satisfiability of ground formulae over a base theory.

Download PDF

This paper extends:

Applications of hierarchical reasoning in the verification of complex systems

Proceedings of the Fourth International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'06), pages 15-26, 2006. Download PDF

Local reasoning in verification

Proceedings of the Verification Workshop VERIFY'06, pages 128-145, 2006.

Abstract: he goal of this paper is to show, concretely, the wide applicability of results on hierarchical reasoning in local theory extensions in verification. We start with an up-to-date survey of our results on reasoning in local theory extensions, ranging from characterizations of locality to interpolation. We then provide several examples, emphasizing theories occurring in a natural way in verification. Finally, we present several applications - some already existing in the literature, others obtained during the work in the AVACS project - where such theories occur in a natural way.

Download PostScript, PDF

Sheaves and geometric logic and applications to modular verification of complex systems

Electronic Notes in Theoretical Computer Science (GETCO 2006), to appear.

Abstract: In this paper we show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space. In this context, geometric logic can be used to describe which local properties, of individual systems, are preserved, at a global level, when interconnecting the systems. The main area of application is to modular verification of complex systems. We illustrate our ideas by means of an example involving a family of interacting controllers for trains on a rail track.

Download PDF

This is the extended version of the following paper:

Sheaves and geometric logic in concurrency

Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006).

Modeling Interaction by Sheaves and Geometric Logic

(together with K. Stokkermans)

Proceedings of FCT'99, (eds. G. Ciobanu and Gh. Paun), 31 August - 3 September 1999, Iasi, LNCS 1684, pages 512-523, Springer Verlag.

Abstract: In this paper we show that, given a family of interacting systems, many notions which are important for expressing properties of systems can be modeled as sheaves over a suitable topological space. In such contexts, geometric logic can be used to test whether ``local'' properties can be lifted to a global level. We develop a way to use this method in the study of interacting systems, illustrated by examples.

Download: PostScript, BibTex-Entry

Towards a Sheaf Semantics for Cooperating Agents Scenarios

AISMC-3, Steyr, September 1996, LNCS 1138, pages 289-304, Springer Verlag, 1996.

Abstract: The ultimate goal of our work is to show how sheaf theory can be used for studying cooperating robotics scenarios. In this paper we propose a formal definition for systems and define a category of systems. The main idea of the paper is that relationships between systems can be expressed by a suitable Grothendieck topology on the category of systems. We show that states and (parallel) actions can be expressed by sheaves and use this in order to study the behavior of systems in time.

Download: PostScript, BibTex-Entry

A Fibered Approach to Modeling Space-Time Dependent Cooperating Agents Scenarios

(together with J. Pfalzgraf and K. Stokkermans)

FAPR'96, Workshop "Reasoning about Actions and Planning in Complex Environments", Bonn, June 1996.

Abstract: In this paper we extend previous work on logical fiberings to situations when space-time dependencies have to be considered. We first introduce the concept of (logical) fiberings and the generic modeling principle. We then illustrate our approach by two examples. The first was implemented as part of the MEDLAR robotics demonstrator and involved a simple 3-robot example. The second example is much more complicated, and takes, for the first time, both space and time dependency into account. We conclude with a brief report on ongoing work on sheaf semantics for cooperating agents scenarios which aims at incorporating such issues and space and time dependency.

Download: BibTex-Entry, PostScript,

On a Semantics for Cooperative Agents Scenarios

(together with J. Pfalzgraf and K. Stokkermans)

Cybernetics and Systems '96, Vol.1 (ed. Trappl, R.), Proceedings of the 13th EMCSR, April 1996, Vienna, pages 201-206, Austrian Society for Cybernetic Studies.

Abstract: The ultimate aim of this work is to find a semantics for reasoning about actions and change in cooperating agent scenarios based on the concept of so called logical fiberings. We formulate a generic modeling principle using this notion. The ideas are illustrated on a simple example. Furthermore we show how these ideas have been used in order to generate a plan that is given as input to the robotics animation program ICARS, available at RISC-Linz. We also sketch the way how a sheaf semantics can be developed for studying cooperating robotics scenarios.

Download: BibTex-Entry

Formula-handling Computer Solution of Boolean Equations. I. Ring Equations

Bull. of the EATCS No. 37 / 1989.

Abstract: We describe a method for solving symbolically Boolean equation by using Loewenheim's theorem, and an implementation in LISP. BibTex-Entry

Duality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part I

Studia Logica 64(1), 93-132, 2000.

Abstract: The main goal of this paper is to explain the link between the algebraic and the Kripke-style models for certain classes of propositional logics. We start by presenting a Priestley-type duality for distributive lattices endowed with a general class of well-behaved operators. We then show that finitely-generated varieties of distributive lattices with operators are closed under canonical embedding algebras. The results are used in the second part of the paper to construct topological and non-topological Kripke-style models for logics that are sound and complete with respect to varieties of distributive lattices with operators in the above-mentioned classes.

Download: preliminary version (PostScript); BibTex-Entry.

Abstract on the Kluwer Academic Publishers Home page (a .pdf file is also available from that page).

Duality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part II

Studia Logica 64(2), 151-172, 2000.

Abstract: In this paper we explain the link between the algebraic models and the Kripke-style models for certain classes of propositional non-classical logics. We consider logics that are sound and complete with respect to varieties of distributive lattices with certain classes of well-behaved operators for which a Priestley-style duality holds, and present a way of constructing topological and non-topological Kripke-style models for these types of logics. Moreover, we show that, under certain additional assumptions on the variety of the algebraic models of the given logics, soundness and completeness with respect to these classes of Kripke-style models follows by using entirely algebraical arguments from the soundness and completeness of the logic with respect to its algebraic models.

Download: preliminary version (PostScript); BibTex-Entry.

Abstract on the Kluwer Academic Publishers Home page (a .pdf file is also available on that page).

Priestley Duality for SHn-Algebras and Applications to the Study of Kripke-Style Models for SHn-Logics

Multiple-Valued Logics, An International Journal 5(4), 281-305, 2000.

Abstract: The main goal of this paper is to show that the Priestley duality for SHn-algebras can help to establish a link between the algebraic and Kripke-style semantics for SHn-logics. We present a Priestley duality theorem for SHn-algebras, and note that the dual space of an SHn-algebra satisfies in particular the properties of a Kripke model for SHn-logics. We then show that Priestley duality can help in proving the soundness and completeness of SHn-logics with respect to the class of SHn-frames in a direct way, by using only soundness and completeness of SHn-logics with respect to the variety of SHn-algebras.

Download: preliminary version (PostScript file); BibTex-Entry.

Priestley representation for distributive lattices with operators and applications to automated theorem proving

Dualities, Interpretability and Ordered Structures, Eds. Julia Vaz de Carvalho and Isabel Ferreirim, Centro de Algebra da Universidade de Lisboa, May 1999 (Proceedings of the Workshop on dualities, interpretability and ordered structures, Lisbon, September 26-27, 1997.)

Abstract: We use the Priestley duality for distributive lattices with operators (DLO) to define a Kripke-style semantics for (fintely-valued) logics based on DLO. This is then used for automated theorem proving in these classes of logics.

Automated reasoning in some local extensions of ordered structures

with Carsten Ihlemann, Journal of Multiple-Valued Logics and Soft Computing, To appear.

Abstract We give a uniform method for automated reasoning in several types of extensions of ordered algebraic structures (definitional extensions, extensions with boundedness axioms or with monotonicity axioms). We show that such extensions are local and, hence, efficient methods for hierarchical reasoning exist in all these cases.

Download: preliminary version PDF.

Automated reasoning in some local extensions of ordered structures

with Carsten Ihlemann, Proceedings of ISMVL'07, IEEE Press, paper 1, 2007.

Abstract We give a uniform method for automated reasoning in several types of extensions of ordered algebraic structures (definitional extensions, extensions with boundedness axioms or with monotonicity axioms). We show that such extensions are local and, hence, efficient methods for hierarchical reasoning exist in all these cases.

Download: preliminary version PDF.

On unification in certain finitely generated varieties of algebras

Proceedings of UNIF 2007,extended abstract.

On unification for Bounded Distributive Lattices

ACM TOCL 8(2), 2007.

Abstract: We give a method for deciding unifiability in the variety of bounded distributive lattices. For this, we reduce the problem of deciding whether a unification problem ${\cal S}$ has a solution to the problem of checking the satisfiability of a set $\Phi_{\cal S}$ of ground clauses. This is achieved by using a structure-preserving translation to clause form. The satisfiability check can then be performed either by a resolution-based theorem prover or by a SAT checker. We apply the method to unification with free constants and to unification with linear constant restrictions, and show that, in fact, it yields a decision procedure for the positive theory of the variety of bounded distributive lattices. We also consider the problem of unification over (i.e.\ in an algebraic extension of) the free lattice. Complexity issues are also addressed.

Download PostScript (ACM TOCL website) PostScript (own version) BibTex-Entry.

Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras

Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004), Toronto, Canada, May 19-22, 2004, IEEE Computer Society, Los Alamitos, 2004, to appear.

Abstract In this paper we give resolution-based decision procedures for the positive theory of certain finitely-generated varieties of algebras. The method is based on the existence of representation theorems for such classes of algebras..

Download: gzipped PostScript, BibTex-Entry

Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators

Journal of Symbolic Computation 36, 6, 891-924, 2003.

Abstract: We establish a link between the satisfiability of universal sentences with respect to classes of distributive lattices with operators and their satisfiability with respect to certain classes of relational structures. This justifies a method for structure-preserving translation to clause form of universal sentences in such classes of algebras. We show that refinements of resolution yield decision procedures for the universal theory of some such classes. In particular, we obtain exponential space and time decision procedures for the universal clause theory of (i) the class of all bounded distributive lattices with operators satisfying a set of (generalized) residuation conditions, (ii) the class of all bounded distributive lattices with operators, and a doubly-exponential time decision procedure for the universal clause theory of the class of all Heyting algebras.

Download: gzipped .ps file, BibTex-Entry.

On uniform word problems involving bridging operators on distributive lattices

Proceedings of TABLEAUX 2002, July 2002, Copenhagen, LNCS 2381, 235-250. Springer, 2002.

Abstract: In this paper we analyze some fragments of the universal theory of distributive lattices with many sorted bridging operators. Our interest in such algebras is motivated by the fact that, in description logics, numerical features are often expressed by using maps that associate numerical values to sets (more generally, to lattice elements). We first establish a link between satisfiability of universal sentences with respect to algebraic models and satisfiability with respect to certain classes of relational structures. We use these results for giving a method for translation to clause form of universal sentences, and provide some decidability results based on the use of resolution or hyperresolution. Links between hyperresolution and tableau methods are also discussed, and a tableau procedure for checking satisfiability of formulae of type $t_1 \leq t_2$ is obtained by using a hyperresolution calculus.

Download: Pdf file, BibTex-Entry.

On unification for Bounded Distributive Lattices

Proceedings of CADE-17, LNAI 1831, pages 465-481, 2000, Springer Verlag.

Abstract: We give a resolution-based procedure for deciding unifiability in the variety of bounded distributive lattices. The algorithm consists of the following steps:

(i) Structure-preserving translation to clause form. Testing the satisfiability of a unification problem $S$ is reduced to the problem of checking the satisfiability of a set $\Phi_S$ of clauses. Expressing $\Phi_S$ as a set of constrained clauses further simplifies the representation of the problem.

(ii) Ordered resolution with selection for (constrained) clauses is used for testing the satisfiability of $\Phi_S$.

Step 1 uses the description of the free bounded distributive lattice over $C$ as the lattice of all upwards-sets of (P(C), \subseteq), which is a consequence of the Priestley representation theorem. We also show that similar ideas can be used for unification with linear constant restrictions. The main advantage of our approach is that it makes it much easier to treat the unification problem for bounded distributive lattices, by using results in resolution theory. Using results of Baader and Schulz, our results also show that resolution can be used for deciding the positive theory of ${\sf D}_{01}$.

Download: PostScript, BibTex-Entry

On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results

Proceedings of CADE-16, LNAI 1632, pages 157-171, Springer Verlag, 1999.

Abstract: In this paper we give a method for automated theorem proving in the universal theory of certain varieties of distributive lattices with well-behaved operators. For this purpose, we use extensions of Priestley's representation theorem for distributive lattices. We first establish a link between satisfiability of universal sentences with respect to varieties of distributive lattices with operators and satisfiability with respect to certain classes of relational structures. We then use these results for giving a method for translation to clause form of universal sentences in such varieties, and obtain decidability and complexity results for the universal theory of some such varieties. The advantage is that we avoid the explicit use of the full algebraic structure of such lattices, instead using sets endowed with a reflexive and transitive relation and with additional functions and relations. We first studied this type of relationships in the context of finitely-valued logics and then extended the ideas to more general non-classical logics. This paper shows that the idea is much more general. In particular, the method presented here subsumes both existing methods for translating modal logics to classical logic and methods for automated theorem proving in finitely-valued logics based on distributive lattices with operators.

Download: PostScript, BibTex-Entry

The results are extended in:

Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators

Research Report MPI-I-2001-2-005 Max-Planck-Institut füormatik, September 2001, ISSN 0946-011X,

On unification in certain finitely generated varieties of algebras

Proceedings of UNIF 2007,extended abstract.

Abstract: We present resolution-based decision procedures for the positive theory of certain finitely-generated varieties of algebras. The method is based on the existence of natural dualities for such classes of algebras.

Download: PDF Proceedings of UNIF 2007.

On unification for Bounded Distributive Lattices

ACM TOCL 8(2), 2007.

Abstract: We give a method for deciding unifiability in the variety of bounded distributive lattices. For this, we reduce the problem of deciding whether a unification problem ${\cal S}$ has a solution to the problem of checking the satisfiability of a set $\Phi_{\cal S}$ of ground clauses. This is achieved by using a structure-preserving translation to clause form. The satisfiability check can then be performed either by a resolution-based theorem prover or by a SAT checker. We apply the method to unification with free constants and to unification with linear constant restrictions, and show that, in fact, it yields a decision procedure for the positive theory of the variety of bounded distributive lattices. We also consider the problem of unification over (i.e.\ in an algebraic extension of) the free lattice. Complexity issues are also addressed.

Download PostScript (ACM TOCL website) PostScript (own version) BibTex-Entry.

Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras

Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004), Toronto, Canada, May 19-22, 2004, IEEE Computer Society, Los Alamitos, 2004.

Abstract In this paper we give resolution-based decision procedures for the positive theory of certain finitely-generated varieties of algebras. The method is based on the existence of representation theorems for such classes of algebras..

Download: gzipped PostScript, BibTex-Entry

On unification for Bounded Distributive Lattices

Proceedings of CADE-17, LNAI 1831, pages 465-481, 2000, Springer Verlag.

Abstract: We give a resolution-based procedure for deciding unifiability in the variety of bounded distributive lattices. The algorithm consists of the following steps:

(i) Structure-preserving translation to clause form. Testing the satisfiability of a unification problem $S$ is reduced to the problem of checking the satisfiability of a set $\Phi_S$ of clauses. Expressing $\Phi_S$ as a set of constrained clauses further simplifies the representation of the problem.

(ii) Ordered resolution with selection for (constrained) clauses is used for testing the satisfiability of $\Phi_S$.

Step 1 uses the description of the free bounded distributive lattice over $C$ as the lattice of all upwards-sets of (P(C), \subseteq), which is a consequence of the Priestley representation theorem. We also show that similar ideas can be used for unification with linear constant restrictions. The main advantage of our approach is that it makes it much easier to treat the unification problem for bounded distributive lattices, by using results in resolution theory. Using results of Baader and Schulz, our results also show that resolution can be used for deciding the positive theory of ${\sf D}_{01}$.

Download: PostScript, BibTex-Entry