Mace4
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Computing finite models by reduction to function-free clause logic
- Directly indecomposables in semidegenerate varieties of connected po-groupoids
- Automated verification of refinement laws
- Constructing infinite models represented by tree automata
- Single identities for lattice theory and for weakly associative lattices
- PyRes
- SETHEO
- RegStab
- RelView
- The existence of Schröder designs with equal-sized holes
- Shortest single axioms for the equivalential calculus with CD and RCD
- Alloy
- LOOPS
- OilEd
- OTTER
- VAMPIRE
- Decomposable constraints
- A set solver for finite set relation algebra
- SPASS
- TPTP
- Darwin
- The Andrews-Curtis conjecture, term rewriting and first-order proofs
- SPASS+T
- Algebras of Ehresmann semigroups and categories
- On derived algebras and subvarieties of implication zroupoids
- Prover9
- The retraction relation for biracks
- Use of logical models for proving infeasibility in term rewriting
- Tactics and certificates in Meta Dedukti
- ProofWatch: watchlist guidance for large theories in E
- Investigating the existence of large sets of idempotent quasigroups via satisfiability testing
- Symmetric implication zroupoids and identities of Bol-Moufang type
- FINDER
- SATCHMO
- SCOTT
- E-Darvin
- ProB
- Kodkod
- E-SETHEO
- Automated reasoning and mathematics. Essays in memory of William W. McCune
- GRAFFITI
- CVC Lite
- RiG
- Smallsemi
- LOOPS
- Ehresmann theory and partition monoids
- CompoSAT: specification-guided coverage for model finding
- Right-orderability versus left-orderability for monoids
- Ehresmann semigroups whose categories are EI and their representation theory
- On quasigroups satisfying Stein's third law
- Equivalence à la Mundici for commutative lattice-ordered monoids
- Ralf
- ARA
- RALL
- KAT-ML
- Semidistributivity and whitman property in implication zroupoids
- \((\mathscr{F},\mathscr{G})\)-abundant semigroups
- Boosting isomorphic model filtering with invariants
- Set of support, demodulation, paramodulation: a historical perspective
- Pardinus: a temporal relational model finder
- Formalization of quasilattices
- Tipi
- On weakly associative lattices and near lattices
- Learning to solve geometric construction problems from images
- Okubo quasigroups
- Learning theorem proving components
- CERES
- iProver-Eq
- An Ehresmann-Schein-Nambooripad type theorem for DRC-semigroups
- MGTP
- iProver
- leanCoP
- Varieties of regular semigroups with uniquely defined inversion
- Herbrand constructivization for automated intuitionistic theorem proving
- Structure theorems for idempotent residuated lattices
- The construction of multipermutation solutions of the Yang-Baxter equation of level 2
- Override and update
- Saigawa
- Relational characterisations of paths
- E Theorem Prover
- Theorem prover for intuitionistic logic based on the inverse method
- MaLARea
- Ivy
- MathWeb
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- FAdo
- GUItar
- PDCoq
- HR
- tptp2X
- The structure of finite commutative idempotent involutive residuated lattices
- Semigroup identities and proofs
- tawSolver
- Proving semantic properties as first-order satisfiability
- The SAT+CAS method for combinatorial search with applications to best matrices
- Using well-founded relations for proving operational termination
- Blocking and other enhancements for bottom-up model generation methods
- Combining induction and saturation-based theorem proving
- Solving quantifier-free first-order constraints over finite sets and binary relations
- GRUNGE: a grand unified ATP challenge
This page was built for software: Mace4
