Mace4
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Sublattices of associahedra and permutohedra
- Structure theorems for idempotent residuated lattices
- Moufang and commutant elements in magmas
- The legacy of a great researcher
- Large theory reasoning with SUMO at CASC
- Unary-determined distributive \(\ell \)-magmas and bunched implication algebras
- The structure of finite commutative idempotent involutive residuated lattices
- Skew lattices and binary operations on functions
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Tool-Based Verification of a Relational Vertex Coloring Program
- Blocking and other enhancements for bottom-up model generation methods
- Herbrand constructivization for automated intuitionistic theorem proving
- Nilpotency in automorphic loops of prime power order.
- Automated Reasoning in Kleene Algebra
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- CompoSAT: specification-guided coverage for model finding
- Admissible Orders of Jordan Loops
- An elegant 3-basis for inverse semigroups.
- Pardinus: a temporal relational model finder
- Set of support, demodulation, paramodulation: a historical perspective
- Theorem prover for intuitionistic logic based on the inverse method
- Primary Decompositions in Varieties of Commutative Diassociative Loops
- Automatic generation of logical models with AGES
- On the axioms of singquandles
- Loops with exponent three in all isotopes
- Searching for shortest single axioms for groups of exponent \(6\)
- Understanding Resolution Proofs through Herbrand’s Theorem
- Relational and multirelational representation theorems for complete idempotent left semirings.
- The extended permutohedron on a transitive binary relation.
- Hopscotch -- reaching the target hop by hop
- Machine learning for first-order theorem proving
- Automatically Proving and Disproving Feasibility Conditions
- mu-term: Verify Termination Properties Automatically (System Description)
- Formalization of quasilattices
- Simple right conjugacy closed loops
- Pure Latin directed triple systems
- The retraction relation for biracks
- All the shortest single axioms for Boolean SQS-skeins.
- The TM system for repairing non-theorems
- Automating Algebraic Specifications of Non-freely Generated Data Types
- Weakening Relation Algebras and FL$$^2$$-algebras
- Treewidth-two graphs as a free algebra
- Types of directed triple systems
- Algebraic notions of nontermination: Omega and divergence in idempotent semirings
- (Dual) hoops have unique halving
- Triple systems and binary operations
- Automatic construction and verification of isotopy invariants
- Mathematical applications of inductive logic programming
- Visual Algebraic Proofs for Unknot Detection
- scientific article; zbMATH DE number 5902401 (Why is no real title available?)
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- System description generating models by SEM
- Reachability as derivability, finite countermodels and verification
- When is the commutant of a Bol loop a subloop?
- Using well-founded relations for proving operational termination
- Minimal paths in the commuting graphs of semigroups
- A set solver for finite set relation algebra
- Lemma Mining over HOL Light
- Independent axiom systems for nearlattices
- Linear groupoids and the associated wreath products.
- On derived algebras and subvarieties of implication zroupoids
- Extended transitive separation logic
- Multirelational representation theorems for complete idempotent left semirings.
- The construction of multipermutation solutions of the Yang-Baxter equation of level 2
- Automated Inference of Finite Unsatisfiability
- Commutative Doubly-Idempotent Semirings Determined by Chains and by Preorder Forests
- Cancellation in skew lattices
- Learning to solve geometric construction problems from images
- Ehresmann theory and partition monoids
- Okubo quasigroups
- Automated inference of finite unsatisfiability
- On Tarski's axiomatic foundations of the calculus of relations
- Foundations of Information and Knowledge Systems
- Superposition for bounded domains
- Performance of clause selection heuristics for saturation-based theorem proving
- Exploring theories with a model-finding assistant
- Enumeration of AG-groupoids.
- The strategy challenge in SMT solving
- Uniqueness of Steiner laws on cubic curves
- Predicting and detecting symmetries in FOL finite model search
- Applying SAT solving in classification of finite algebras
- Automatic proofs and counterexamples for some ortholattice identities
- Order in implication zroupoids
- Developments in concurrent Kleene algebra
- Commutator theory for loops.
- Lemma Learning in the Model Evolution Calculus
- scientific article; zbMATH DE number 5170267 (Why is no real title available?)
- Semigroup identities and proofs
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
- \((\mathscr{F},\mathscr{G})\)-abundant semigroups
- Use of logical models for proving infeasibility in term rewriting
- Override and update
- The commingling of commutativity and associativity in Bol loops.
- Shortening of proof length is elusive for theorem provers
- A note on regular De Morgan semi-Heyting algebras
- Incidence properties of cosets in loops.
- Algebraic separation logic
- Concurrent Kleene algebra and its foundations
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Computing finite models by reduction to function-free clause logic
This page was built for software: Mace4
