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
• Unary-determined distributive \(\ell \)-magmas and bunched implication algebras
• The structure of finite commutative idempotent involutive residuated lattices
• Automated reasoning with power maps
• Tool-Based Verification of a Relational Vertex Coloring Program
• Primary Decompositions in Varieties of Commutative Diassociative Loops
• Understanding Resolution Proofs through Herbrand’s Theorem
• Commutativity theorems in groups with power-like maps
• Searching for shortest single axioms for groups of exponent \(6\)
• Automatically Proving and Disproving Feasibility Conditions
• mu-term: Verify Termination Properties Automatically (System Description)
• Visual Algebraic Proofs for Unknot Detection
• A set solver for finite set relation algebra
• Independent axiom systems for nearlattices
• Superposition for bounded domains
• Loops with abelian inner mapping groups: an application of automated deduction
• Ehresmann theory and partition monoids
• Performance of clause selection heuristics for saturation-based theorem proving
• Formalizing a fragment of combinatorics on words
• \((\mathscr{F},\mathscr{G})\)-abundant semigroups
• Use of logical models for proving infeasibility in term rewriting
• A class of loops categorically isomorphic to Bruck loops of odd order.
• Teaching Automated Theorem Proving by Example: PyRes 1.2
• Steps toward a computational metaphysics
• Equivalence à la Mundici for commutative lattice-ordered monoids
• Directly indecomposables in semidegenerate varieties of connected po-groupoids
• Cardinality of relations and relational approximation algorithms
• Varieties of regular semigroups with uniquely defined inversion
• Relational characterisations of paths
• THE MOUFANG LAWS, GLOBAL AND LOCAL

This page was built for software: Prover9