Algèbre de Boole (structure) | EPFL Graph Search

vignette|Exemple d'algèbre de Boole : l'ensemble des parties de l'ensemble {x, y, z} illustré par son diagramme de Hasse. En mathématiques, une algèbre de Boole, ou parfois anneau de Boole, est une structure algébrique étudiée en particulier en logique mathématique. Une algèbre de Boole peut être définie soit comme une structure ordonnée particulière, soit comme une structure algébrique particulière, soit comme un anneau (unitaire) dont tout élément égale son carré. Pour tout ensemble, l'ensemble de ses parties est une algèbre de Boole, l'ordre associé étant l'inclusion et les lois d'anneau la différence symétrique et l'intersection. Un autre exemple est donné par l'ensemble des formules du calcul propositionnel prises à équivalence (en logique classique) près (sur un nombre de variables de cardinal arbitraire), l'ordre associé étant la relation de conséquence logique et les lois d'anneau la disjonction exclusive et la conjonction. Définitions Algèbre de Boole comme

On Polynomial Algorithms for Normalizing Formulas

Mario Bucev, Simon Guilloud, Viktor Kuncak

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem for two subtheories of Boolean algebra, giving a sound procedure for propositional logical equivalence that is incomplete in general but complete with respect to a subset of Boolean algebra axioms. We first show a new algorithm to produce a normal form for expressions in the theory of ortholattices (OL) in time O(n^2). We also consider an algorithm, recently presented but never evaluated in practice, producing a normal form for a slightly weaker theory, orthocomplemented bisemilattices (OCBSL), in time O(n log(n)^2). For both algorithms, we present an implementation and show efficiency in two domains. First, we evaluate the algorithms on large propositional expressions, specifically combinatorial circuits from a benchmark suite, as well as on large random formulas. Second, we implement and evaluate the algorithms in the Stainless verifier, a tool for verifying the correctness of Scala programs. We used these algorithms as a basis for a new formula simplifier, which is applied before valid verification conditions are saved into a persistent cache. The results show that normalization substantially increases cache hit ratio in large benchmarks.

2022

Unique decomposition of homogeneous languages and application to isothetic regions

Nicolas René Jean Ninin

A language is said to be homogeneous when all its words have the same length. Homogeneous languages thus form a monoid under concatenation. It becomes freely commutative under the simultaneous actions of every permutation group G(n) on the collection of homogeneous languages of length n is an element of N. One recovers the isothetic regions from (Haucourt 2017, to appear (online since October 2017)) by considering the alphabet of connected subsets of the space vertical bar G vertical bar, viz the geometric realization of a finite graph G. Factoring the geometric model of a conservative program amounts to parallelize it, and there exists an efficient factoring algorithm for isothetic regions. Yet, from the theoretical point of view, one wishes to go beyond the class of conservative programs, which implies relaxing the finiteness hypothesis on the graph G. Provided that the collections of n-dimensional isothetic regions over G (denoted by R-n vertical bar G vertical bar) are co -unital distributive lattices, the prime decomposition of isothetic regions is given by an algorithm which is, unfortunately, very inefficient. Nevertheless, if the collections R-n vertical bar G vertical bar satisfy the stronger property of being Boolean algebras, then the efficient factoring algorithm is available again. We relate the algebraic properties of the collections R-n vertical bar G vertical bar to the geometric properties of the space I GI. On the way, the algebraic structure R-n vertical bar G vertical bar is proven to be the universal tensor product, in the category of semilattices with zero, of n copies of the algebraic structure R-1 vertical bar G vertical bar.

2019

The use of Boolean concepts in general classification contexts

Luis Miguel Moreira

Data classification, in the present context, concerns the use of computers in order to create systems that learn how to automatically decide to which of a predefined set of classes a given object belongs. Boolean concepts have long been present in data classification, and still are today, at various levels. We consider a kind of Boolean elements, called patterns, which consist of specific conjunctions of Boolean facts. Assuming the existence of two classes of objects, the positive and the negative, patterns can be expressed as conditionals of the type "If A and B and not C, then positive", where A, B, and C are Boolean values, each associated with a specific attribute describing the objects to be classified. From the classification system point of view, patterns are basic Boolean expressions that can be processed in a purely mathematical manner. However, if the values of the conjunction have an intuitive meaning, then this type of representation provides an intuitive perspective of the classification system, which can be interpreted by humans. The use of sets of patterns for building classification systems is justified by the fact that certain conjunctions of the type described above are matched by objects of one class but not by those of the other class. In this sense, patterns possess distinguishing properties that can be used to determine whether an object belongs to a class (if it matches certain patterns) or not. In this thesis, we consider the use of classification systems based on patterns, which we have seen to be inherently Boolean, in the context of classification tasks where nothing is Boolean, that is to say, where the objects are described by multi-valued or continuous attributes and instead of a positive/negative decision, suitable to situations where only two classes are involved, the output is rather the selection of a class among several. The work presented here extends along different directions. It starts by the study of a suitable way of transforming the attributes describing the objects to be classified into equivalent Boolean attributes. We describe the constraints that must be satisfied by this transformation and present a procedure allowing it to be done in a short amount of time. Another research direction explores the possibility of generating multi-class divisions with systems whose output is Boolean. This study has the benefit of also being applicable to other types of classification systems adapted to two-class situations, but whose internal language is not necessarily Boolean. This is the case of some current state-of-the-art systems. To realize this adaptation, the common approach consists in decomposing the original problem into several two-class sub-problems and generating an independent classification system to solve each one of them. The final class decision is obtained from the combination of the partial Boolean decisions. We analyze and compare several existing procedures for this purpose, and in addition propose an interesting new procedure. Finally, we consider the possibility of sharing patterns among several classes and develop a Boolean-based classification system which is directly adapted to multi-class problems, but maintaining the property of being understandable by humans. We show that the performance of this type of system is not in all cases comparable to the best available systems, but they have the advantage of providing, in certain circumstances, a better understanding of the problem at hand.

EPFL2000

The use of Boolean concepts in general classification contexts

Luis Miguel Moreira

EPFL2000