Prover9

swMATH4969MaRDI QIDQ17116FDOQ17116

Author name not available (Why is that?)

Official website: http://www.cs.unm.edu/~mccune/prover9/

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

• Axiomatizing the skew Boolean propositional calculus
• Sublattices of associahedra and permutohedra
• The structure of finite commutative idempotent involutive residuated lattices
• Tool-Based Verification of a Relational Vertex Coloring Program
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Nilpotency in automorphic loops of prime power order.
• An elegant 3-basis for inverse semigroups.
• Combinatorics_Words
• Tarski geometry axioms. III
• Understanding Resolution Proofs through Herbrand’s Theorem
• Searching for shortest single axioms for groups of exponent \(6\)
• 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
• Lemma Mining over HOL Light
• On derived algebras and subvarieties of implication zroupoids
• Automated Inference of Finite Unsatisfiability
• 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
• Formalizing a fragment of combinatorics on words
• Shortening of proof length is elusive for theorem provers
• \((\mathscr{F},\mathscr{G})\)-abundant semigroups
• Dependently-typed formalisation of relation-algebraic abstractions
• Towards an algebra of routing tables
• Projective bichains
• Steps toward a computational metaphysics
• Cardinality of relations and relational approximation algorithms
• Constructions of commutative automorphic loops.
• Algebraic calculi for hybrid systems
• The structure of commutative automorphic loops.
• Automated flaw detection in algebraic specifications
• Algebras of Ehresmann semigroups and categories
• Weak bisimulation for coalgebras over order enriched monads
• Semisimples in varieties of commutative integral bounded residuated lattices
• Complete axiomatizations for XPath fragments
• The structure of automorphic loops
• Half-isomorphisms of Moufang loops.
• On automated program construction and verification
• 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
• Domain and antidomain semigroups
• Inverse semigroups with idempotent-fixing automorphisms.
• Learning-assisted theorem proving with millions of lemmas
• The algebra of functions with antidomain and range
• Deciding regular expressions (in-)equivalence in Coq
• Connected quandles associated with pointed abelian groups
• Automated verification of relational while-programs
• On Automating the Calculus of Relations
• Tarski geometry axioms. II
• Ken Kunen: algebraist.
• Algebraic neighbourhood logic
• Constructive logic with strong negation is a substructural logic. II
• 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
• Non-commutative propositional logic with short-circuit evaluation
• Proof simplification and automated theorem proving
• On implicator groupoids
• Varieties of Birkhoff systems. I
• Structure theorems for idempotent residuated lattices
• Unary-determined distributive \(\ell \)-magmas and bunched implication algebras
• Automated reasoning with power maps
• Old or heavy? Decaying gracefully with age/weight shapes
• Primary Decompositions in Varieties of Commutative Diassociative Loops
• 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
• Commutativity theorems in groups with power-like maps
• Automatically Proving and Disproving Feasibility Conditions
• mu-term: Verify Termination Properties Automatically (System Description)
• Simply connected Latin quandles
• Formalization of quasilattices
• Treewidth-two graphs as a free algebra
• Visual Algebraic Proofs for Unknot Detection
• Pappus's hexagon theorem in real projective plane
• On two alternative axiomatizations of lattices by McKenzie and Sholander
• A set solver for finite set relation algebra
• Independent axiom systems for nearlattices
• The construction of multipermutation solutions of the Yang-Baxter equation of level 2
• Learning to solve geometric construction problems from images
• Ehresmann theory and partition monoids
• Override and update
• 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
• Equivalence à la Mundici for commutative lattice-ordered monoids
• Directly indecomposables in semidegenerate varieties of connected po-groupoids
• Varieties of regular semigroups with uniquely defined inversion
• Relational characterisations of paths
• THE MOUFANG LAWS, GLOBAL AND LOCAL
• Ehresmann semigroups whose categories are EI and their representation theory

This page was built for software: Prover9