Prover9

swMATH4969MaRDI QIDQ17116FDOQ17116

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Axiomatizing the skew Boolean propositional calculus
• Sublattices of associahedra and permutohedra
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Automated Reasoning in Kleene Algebra
• Herbrand constructivization for automated intuitionistic theorem proving
• Nilpotency in automorphic loops of prime power order.
• An elegant 3-basis for inverse semigroups.
• Automatic generation of logical models with AGES
• Tarski geometry axioms. III
• Machine learning for first-order theorem proving
• 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
• The retraction relation for biracks
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Algebraic notions of nontermination: Omega and divergence in idempotent semirings
• Complementation in representable theories of region-based space
• Permutation of elements in double semigroups
• 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
• Order in implication zroupoids
• Developments in concurrent Kleene algebra
• 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
• Internal axioms for domain semirings
• Dependently-typed formalisation of relation-algebraic abstractions
• Towards an algebra of routing tables
• Projective bichains
• On hom-algebras with surjective twisting
• Constructions of commutative automorphic loops.
• Algebraic calculi for hybrid systems
• The structure of commutative automorphic loops.
• 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.
• Weak bisimulation for coalgebras over order enriched monads
• Type-2 fuzzy sets and bichains
• Generalised domain and \(E\)-inverse semigroups
• Semisimples in varieties of commutative integral bounded residuated lattices
• The structure of automorphic loops
• Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
• Foundations of concurrent Kleene algebra
• Constructive logic with strong negation is a substructural logic. I
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• Relational lattices via duality
• Domain and antidomain semigroups
• Inverse semigroups with idempotent-fixing automorphisms.
• Learning-assisted theorem proving with millions of lemmas
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Connected quandles associated with pointed abelian groups
• Automated verification of relational while-programs
• On Automating the Calculus of Relations
• Modal algebra and Petri nets
• Semisimple varieties of implication zroupoids
• Tarski geometry axioms. II
• Ken Kunen: algebraist.
• Relation algebra, RelView, and plurality voting
• A timed process algebra for wireless networks with an application in routing (extended abstract)
• Latin directed triple systems
• Algebraic structures in the vicinity of pre-rough algebra and their logics
• Transitive Separation Logic
• ProofWatch: watchlist guidance for large theories in E
• nanoCoP: a non-clausal connection prover
• Concurrent Kleene Algebra
• On implicator groupoids
• Varieties of Birkhoff systems. I
• Skew lattices and binary operations on functions
• Old or heavy? Decaying gracefully with age/weight shapes
• 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
• Loops with exponent three in all isotopes
• Relational and multirelational representation theorems for complete idempotent left semirings.
• Simply connected Latin quandles
• Formalization of quasilattices
• Treewidth-two graphs as a free algebra
• Pappus's hexagon theorem in real projective plane
• On two alternative axiomatizations of lattices by McKenzie and Sholander
• 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
• 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
• On Tarski's axiomatic foundations of the calculus of relations
• Learning to solve geometric construction problems from images
• The strategy challenge in SMT solving
• Semigroup identities and proofs
• The commingling of commutativity and associativity in Bol loops.
• Override and update
• Title not available (Why is that?)

This page was built for software: Prover9