Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userClone Theory and Algebraic Logic
119
0
0.0
(
0
)
Added by
Zhaohua Luo
Publication date
2009
fields
Informatics Engineering
and research's language is
English
Authors
Zhaohua Luo
Ask ChatGPT about the research
No Arabic abstract
The concept of a clone is central to many branches of mathematics, such as universal algebra, algebraic logic, and lambda calculus. Abstractly a clone is a category with two objects such that one is a countably infinite power of the other. Left and right algebras over a clone are covariant and contravariant functors from the category to that of sets respectively. In this paper we show that first-order logic can be studied effectively using the notions of right and left algebras over a clone. It is easy to translate the classical treatment of logic into our setting and prove all the fundamental theorems of first-order theory algebraically.
rate research
Read More
The primary goal of this paper is to present a unified way to transform the syntax of a logic system into certain initial algebraic structure so that it can be studied algebraically. The algebraic structures which one may choose for this purpose are various clones over a full subcategory of a category. We show that the syntax of equational logic, lambda calculus and first order logic can be represented as clones or right algebras of clones over the set of positive integers. The semantics is then represented by structures derived from left algebras of these clones.
Algebraic logic studies algebraic theories related to proposition and first-order logic. A new algebraic approach to first-order logic is sketched in this paper. We introduce the notion of a quantifier theory, which is a functor from the category of a monad of sets to the category of Boolean algebras, together with a uniquely determined system of quantifiers. A striking feature of this approach is that Cayleys Completeness Theorem and Godels Completeness Theorem can be stated and proved in a much simpler fashion for quantifier theories. Both theorems are due to Halmos for polyadic algebras. We also present a simple transparent treatment of ultraproducts of models of a quantifier theory.
Algebraic characterization of logic programs has received increasing attention in recent years. Researchers attempt to exploit connections between linear algebraic computation and symbolic computation in order to perform logical inference in large scale knowledge bases. This paper proposes further improvement by using sparse matrices to embed logic programs in vector spaces. We show its great power of computation in reaching the fixpoint of the immediate consequence operator from the initial vector. In particular, performance for computing the least models of definite programs is dramatically improved in this way. We also apply the method to the computation of stable models of normal programs, in which the guesses are associated with initial matrices, and verify its effect when there are small numbers of negation. These results show good enhancement in terms of performance for computing consequences of programs and depict the potential power of tensorized logic programs.
The first-order theory of finite and infinite trees has been studied since the eighties, especially by the logic programming community. Following Djelloul, Dao and Fruhwirth, we consider an extension of this theory with an additional predicate for finiteness of trees, which is useful for expressing properties about (not just datatypes but also) codatatypes. Based on their work, we present a simplification procedure that determines whether any given (not necessarily closed) formula is satisfiable, returning a simplified formula which enables one to read off all possible models. Our extension makes the algorithm usable for algebraic (co)datatypes, which was impossible in their original work due to restrictive assumptions. We also provide a prototype implementation of our simplification procedure and evaluate it on instances from the SMT-LIB.
There exists a rich literature of rule formats guaranteeing different algebraic properties for formalisms with a Structural Operational Semantics. Moreover, there exist a few approaches for automatically deriving axiomatizations characterizing strong bisimilarity of processes. To our knowledge, this literature has never been extended to the setting with data (e.g. to model storage and memory). We show how the rule formats for algebraic properties can be exploited in a generic manner in the setting with data. Moreover, we introduce a new approach for deriving sound and ground-complete axiom schemata for a notion of bisimilarity with data, called stateless bisimilarity, based on intuitive auxiliary function symbols for handling the store component. We do restrict, however, the axiomatization to the setting where the store component is only given in terms of constants.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
