Open Access. Powered by Scholars. Published by Universities.®
- Discipline
- Keyword
-
- Axiom system (1)
- Boolean functions (1)
- Boolean matching (1)
- Calculus of relations (1)
- Canonical form (1)
-
- Category Theory (1)
- Classification algorithms (1)
- Cofactor signature (1)
- Computer Science (1)
- Cut elimination (1)
- Decidability (1)
- Field programmable gate arrays (1)
- Finite embeddability property (1)
- Finite model property (1)
- Gentzen system (1)
- Heuristic algorithms (1)
- Independence model (1)
- Independent axiom system (1)
- Input variables (1)
- Libraries (1)
- Logic in Computer Science (1)
- Mathematics (1)
- Multi-type methodology (1)
- NPN classification (1)
- Proper display calculus (1)
- Relation algebra (1)
- Residuated frame (1)
- Residuated lattice (1)
- Runtime (1)
- Semi De Morgan algebras (1)
Articles 1 - 7 of 7
Full-Text Articles in Logic and Foundations
Semi De Morgan Logic Properly Displayed, Giuseppe Greco, Fei Qin, M. Andrew Moshier, Alessandra Palmigiano
Semi De Morgan Logic Properly Displayed, Giuseppe Greco, Fei Qin, M. Andrew Moshier, Alessandra Palmigiano
Mathematics, Physics, and Computer Science Faculty Articles and Research
In the present paper, we endow semi De Morgan logic and a family of its axiomatic extensions with proper multi-type display calculi which are sound, complete, conservative, and enjoy cut elimination and subformula property. Our proposal builds on an algebraic analysis of the variety of semi De Morgan algebras, and applies the guidelines of the multi-type methodology in the design of display calculi.
Extending Set Functors To Generalised Metric Spaces, Adriana Balan, Alexander Kurz, Jiří Velebil
Extending Set Functors To Generalised Metric Spaces, Adriana Balan, Alexander Kurz, Jiří Velebil
Mathematics, Physics, and Computer Science Faculty Articles and Research
For a commutative quantale V, the category V-cat can be perceived as a category of generalised metric spaces and non-expanding maps. We show that any type constructor T (formalised as an endofunctor on sets) can be extended in a canonical way to a type constructor TV on V-cat. The proof yields methods of explicitly calculating the extension in concrete examples, which cover well-known notions such as the Pompeiu-Hausdorff metric as well as new ones.
Conceptually, this allows us to to solve the same recursive domain equation X ≅ TX in different categories (such as sets and metric spaces) and …
Fast Adjustable Npn Classification Using Generalized Symmetries, Xuegong Zhou, Lingli Wang, Peiyi Zhao, Alan Mishchenko
Fast Adjustable Npn Classification Using Generalized Symmetries, Xuegong Zhou, Lingli Wang, Peiyi Zhao, Alan Mishchenko
Mathematics, Physics, and Computer Science Faculty Articles and Research
NPN classification of Boolean functions is a powerful technique used in many logic synthesis and technology mapping tools in FPGA design flows. Computing the canonical form of a function is the most common approach of Boolean function classification. In this paper, a novel algorithm for computing NPN canonical form is proposed. By exploiting symmetries under different phase assignments and higher-order symmetries of Boolean functions, the search space of NPN canonical form computation is pruned and the runtime is dramatically reduced. The algorithm can be adjusted to be a slow exact algorithm or a fast heuristic algorithm with lower quality. For …
On Tarski's Axiomatic Foundations Of The Calculus Of Relations, Hajnal Andréka, Steven Givant, Peter Jipsen, István Németi
On Tarski's Axiomatic Foundations Of The Calculus Of Relations, Hajnal Andréka, Steven Givant, Peter Jipsen, István Németi
Mathematics, Physics, and Computer Science Faculty Articles and Research
It is shown that Tarski’s set of ten axioms for the calculus of relations is independent in the sense that no axiom can be derived from the remaining axioms. It is also shown that by modifying one of Tarski’s axioms slightly, and in fact by replacing the right-hand distributive law for relative multiplication with its left-hand version, we arrive at an equivalent set of axioms which is redundant in the sense that one of the axioms, namely the second involution law, is derivable from the other axioms. The set of remaining axioms is independent. Finally, it is shown that if …
Relation Algebras, Idempotent Semirings And Generalized Bunched Implication Algebras, Peter Jipsen
Relation Algebras, Idempotent Semirings And Generalized Bunched Implication Algebras, Peter Jipsen
Mathematics, Physics, and Computer Science Faculty Articles and Research
This paper investigates connections between algebraic structures that are common in theoretical computer science and algebraic logic. Idempotent semirings are the basis of Kleene algebras, relation algebras, residuated lattices and bunched implication algebras. Extending a result of Chajda and Länger, we show that involutive residuated lattices are determined by a pair of dually isomorphic idempotent semirings on the same set, and this result also applies to relation algebras. Generalized bunched implication algebras (GBI-algebras for short) are residuated lattices expanded with a Heyting implication. We construct bounded cyclic involutive GBI-algebras from so-called weakening relations, and prove that the class of weakening …
Kolmogorov’S Axioms For Probabilities With Values In Hyperbolic Numbers, Daniel Alpay, M. E. Luna-Elizarrarás, Michael Shapiro
Kolmogorov’S Axioms For Probabilities With Values In Hyperbolic Numbers, Daniel Alpay, M. E. Luna-Elizarrarás, Michael Shapiro
Mathematics, Physics, and Computer Science Faculty Articles and Research
We introduce the notion of a probabilistic measure which takes values in hyperbolic numbers and which satisfies the system of axioms generalizing directly Kolmogorov’s system of axioms. We show that this new measure verifies the usual properties of a probability; in particular, we treat the conditional hyperbolic probability and we prove the hyperbolic analogues of the multiplication theorem, of the law of total probability and of Bayes’ theorem. Our probability may take values which are zero–divisors and we discuss carefully this peculiarity.
Residuated Frames With Applications To Decidability, Nikolaos Galatos, Peter Jipsen
Residuated Frames With Applications To Decidability, Nikolaos Galatos, Peter Jipsen
Mathematics, Physics, and Computer Science Faculty Articles and Research
Residuated frames provide relational semantics for substructural logics and are a natural generalization of Kripke frames in intuitionistic and modal logic, and of phase spaces in linear logic. We explore the connection between Gentzen systems and residuated frames and illustrate how frames provide a uniform treatment for semantic proofs of cut-elimination, the finite model property and the finite embeddability property, which imply the decidability of the equational/universal theories of the associated residuated lattice-ordered groupoids. In particular these techniques allow us to prove that the variety of involutive FL-algebras and several related varieties have the finite model property.