Cited in
(only showing first 100 items - show all)- Group embedding of the projective plane \(PG(2, 3)\)
- Axiomatizing the skew Boolean propositional calculus
- Sublattices of associahedra and permutohedra
- Structure theorems for idempotent residuated lattices
- Moufang and commutant elements in magmas
- Semantic Guidance for Saturation Provers
- Unary-determined distributive \(\ell \)-magmas and bunched implication algebras
- Automated reasoning with power maps
- 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
- Old or heavy? Decaying gracefully with age/weight shapes
- Herbrand constructivization for automated intuitionistic theorem proving
- Nilpotency in automorphic loops of prime power order.
- Automated Reasoning in Kleene Algebra
- An elegant 3-basis for inverse semigroups.
- A Wos Challenge Met
- Larry Wos: visions of automated reasoning
- Pardinus: a temporal relational model finder
- Set of support, demodulation, paramodulation: a historical perspective
- Guiding an automated theorem prover with neural rewriting
- 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
- Tarski geometry axioms. III
- 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.
- Computing minimal extending sets by relation-algebraic modeling and development
- Hopscotch -- reaching the target hop by hop
- Machine learning for first-order theorem proving
- Commutativity theorems in groups with power-like maps
- Automatically Proving and Disproving Feasibility Conditions
- mu-term: Verify Termination Properties Automatically (System Description)
- Formalization of quasilattices
- Simple right conjugacy closed loops
- scientific article; zbMATH DE number 7471704 (Why is no real title available?)
- The retraction relation for biracks
- All the shortest single axioms for Boolean SQS-skeins.
- Simply connected Latin quandles
- Automating Algebraic Specifications of Non-freely Generated Data Types
- Weakening Relation Algebras and FL$$^2$$-algebras
- Treewidth-two graphs as a free algebra
- Algebraic notions of nontermination: Omega and divergence in idempotent semirings
- (Dual) hoops have unique halving
- Visual Algebraic Proofs for Unknot Detection
- scientific article; zbMATH DE number 5902401 (Why is no real title available?)
- Pappus's hexagon theorem in real projective plane
- Complementation in representable theories of region-based space
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- Reachability as derivability, finite countermodels and verification
- Permutation of elements in double semigroups
- 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
- On derived algebras and subvarieties of implication zroupoids
- Extended transitive separation logic
- Multirelational representation theorems for complete idempotent left semirings.
- Investigating and computing bipartitions with algebraic means
- 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
- Learning to solve geometric construction problems from images
- Ehresmann theory and partition monoids
- On Tarski's axiomatic foundations of the calculus of relations
- Superposition for bounded domains
- Loops with abelian inner mapping groups: an application of automated deduction
- Performance of clause selection heuristics for saturation-based theorem proving
- The strategy challenge in SMT solving
- Order in implication zroupoids
- Developments in concurrent Kleene algebra
- Formalizing a fragment of combinatorics on words
- Semigroup identities and proofs
- \((\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
- Algebraic separation logic
- Concurrent Kleene algebra and its foundations
- Distributive groupoids are symmetric-by-medial: an elementary proof.
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Internal axioms for domain semirings
- A class of loops categorically isomorphic to Bruck loops of odd order.
- Learning theorem proving components
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Projective bichains
- Dependently-typed formalisation of relation-algebraic abstractions
- Towards an algebra of routing tables
- Semiautomorphic inverse property loops
- Steps toward a computational metaphysics
- Detecting Unknots via Equational Reasoning, I: Exploration
This page was built for software: Prover9
