Mace4

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