1 - 4 of 4 articles
Symmetries abound in logically formulated problems where many axioms are universally quantified, as this is the case in equational theories. Two complementary approaches have been used so far to dynamically tackle those symmetries: prediction and detection. The best-known predictive symmetry...
We describe an algorithm for deciding the first-order multisorted theory BAPA, which combines Boolean algebras of sets of uninterpreted elements (BA) and Presburger arithmetic operations (PA). BAPA can express the relationship between integer variables and cardinalities of unbounded finite sets,...
In this note, we study shortest (with respect to the number of variable occurrences on the left-hand side) possible single axioms for groups of exponent 6 of the form T = x, where T is a term in product only. These investigations were carried out with the automated theorem provers OTTER and...
We explain a computer formulation of Gabriel–Zisman’s localization of categories in the proof assistant Coq. This includes the general localization construction with the proof of Lemma 1.2 of Gabriel and Zisman, as well as the construction using calculus of fractions.
Read and print from thousands of top scholarly journals.
Continue with Facebook
Log in with Microsoft
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Sign Up Log In
To subscribe to email alerts, please log in first, or sign up for a DeepDyve account if you don’t already have one.
To get new article updates from a journal on your personalized homepage, please log in first, or sign up for a DeepDyve account if you don’t already have one.