Mace4
From MaRDI portal
Software:18972
swMATH6905MaRDI QIDQ18972FDOQ18972
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Skew lattices and binary operations on functions
- Blocking and other enhancements for bottom-up model generation methods
- Pardinus: a temporal relational model finder
- Set of support, demodulation, paramodulation: a historical perspective
- Theorem prover for intuitionistic logic based on the inverse method
- Loops with exponent three in all isotopes
- Automatically Proving and Disproving Feasibility Conditions
- mu-term: Verify Termination Properties Automatically (System Description)
- Formalization of quasilattices
- System description generating models by SEM
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- When is the commutant of a Bol loop a subloop?
- Using well-founded relations for proving operational termination
- The construction of multipermutation solutions of the Yang-Baxter equation of level 2
- Learning to solve geometric construction problems from images
- Okubo quasigroups
- Ehresmann theory and partition monoids
- MACE4 and SEM: A Comparison of Finite Model Generators
- Semigroup identities and proofs
- Override and update
- Title not available (Why is that?)
- An Algorithm for Approximating the Satisfiability Problem of High-level Conditions
- Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach
- Learning theorem proving components
- Skew lattices and set-theoretic solutions of the Yang-Baxter equation
- Equivalence à la Mundici for commutative lattice-ordered monoids
- Moufang semidirect products of loops with groups and inverse property extensions
- An Ehresmann-Schein-Nambooripad type theorem for DRC-semigroups
- Ehresmann semigroups whose categories are EI and their representation theory
- On quasigroups satisfying Stein's third law
- GRUNGE: a grand unified ATP challenge
- On weakly associative lattices and near lattices
- Finding Finite Models in Multi-sorted First-Order Logic
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Tactics and certificates in Meta Dedukti
- The Legacy of a Great Researcher
- Algebraic Investigation of Connected Components
- The commingling of commutativity and associativity in Bol loops
- Moufang and commutant elements in magmas
- Automated reasoning and mathematics. Essays in memory of William W. McCune
- Short identities implying a quasigroup is a loop or group.
- Proving semantic properties as first-order satisfiability
- The SAT+CAS method for combinatorial search with applications to best matrices
- Title not available (Why is that?)
- Symmetric implication zroupoids and weak associative laws
- Finite reasons for safety
- Distributivity in Ł\(_{\aleph_0}\) and other sentential logics
- Nonassociative right hoops
- Boosting isomorphic model filtering with invariants
- Second-order properties of undirected graphs
- Agglomerative algebras
- ON TARSKI’S AXIOMATIC FOUNDATIONS OF THE CALCULUS OF RELATIONS
- The hyper tableaux calculus with equality and an application to finite model computation
- Combining induction and saturation-based theorem proving
- Sublattices of associahedra and permutohedra
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Automated Reasoning in Kleene Algebra
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Herbrand constructivization for automated intuitionistic theorem proving
- CompoSAT: specification-guided coverage for model finding
- Nilpotency in automorphic loops of prime power order.
- An elegant 3-basis for inverse semigroups.
- Automatic generation of logical models with AGES
- A Timed Process Algebra for Wireless Networks with an Application in Routing
- Machine learning for first-order theorem proving
- The extended permutohedron on a transitive binary relation.
- Hopscotch -- reaching the target hop by hop
- The retraction relation for biracks
- Automating Algebraic Specifications of Non-freely Generated Data Types
- Algebraic notions of nontermination: Omega and divergence in idempotent semirings
- Automatic construction and verification of isotopy invariants
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Lemma Mining over HOL Light
- Minimal paths in the commuting graphs of semigroups
- On derived algebras and subvarieties of implication zroupoids
- Automated Inference of Finite Unsatisfiability
- Cancellation in skew lattices
- Lemma Learning in the Model Evolution Calculus
- Title not available (Why is that?)
- Automated inference of finite unsatisfiability
- Automatic proofs and counterexamples for some ortholattice identities
- Order in implication zroupoids
- Developments in concurrent Kleene algebra
- Commutator theory for loops.
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
- A note on regular De Morgan semi-Heyting algebras
- Algebraic separation logic
- Concurrent Kleene algebra and its foundations
- Internal axioms for domain semirings
- Relational Lattices via Duality
- Investigating the existence of large sets of idempotent quasigroups via satisfiability testing
- Projective bichains
- Algebras for iteration and infinite computations
- On hom-algebras with surjective twisting
- Automated Verification of Relational While-Programs
- Expansions of semi-Heyting algebras. I: Discriminator varieties
- Automated verification of refinement laws
- Automated flaw detection in algebraic specifications
- A natural characterization of semilattices of rectangular bands and groups of exponent two.
- On First-Order Model-Based Reasoning
This page was built for software: Mace4