Prover9
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Algebraic neighbourhood logic
- Axioms for lattices and Boolean algebras
- Ehresmann semigroups whose categories are EI and their representation theory
- The Andrews-Curtis conjecture, term rewriting and first-order proofs
- Combining induction and saturation-based theorem proving
- Unary-determined distributive \(\ell \)-magmas and bunched implication algebras
- Pappus's hexagon theorem in real projective plane
- Short identities implying a quasigroup is a loop or group.
- Automated deduction in ring theory
- Varieties of regular semigroups with uniquely defined inversion
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- Visual Algebraic Proofs for Unknot Detection
- The algebra of functions with antidomain and range
- Gibbard's collapse theorem for the indicative conditional: an axiomatic approach
- A Hierarchy of Algebras for Boolean Subsets
- Half-isomorphisms of Moufang loops.
- Symmetric implication zroupoids and weak associative laws
- Automated reasoning with power maps
- A set solver for finite set relation algebra
- Simply connected Latin quandles
- Constructive logic with strong negation is a substructural logic. II
- A class of loops categorically isomorphic to Bruck loops of odd order.
- Formalization of quasilattices
- Automated Reasoning for Hybrid Systems — Two Case Studies —
- Relational characterisations of paths
- Agglomerative algebras
- Independent axiom systems for nearlattices
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Knowledge and Games in Modal Semirings
- Equivalence à la Mundici for commutative lattice-ordered monoids
- Commutativity theorems in groups with power-like maps
- ACER
- PyRes
- Primary Decompositions in Varieties of Commutative Diassociative Loops
- Semidistributivity and whitman property in implication zroupoids
- Deciding Kleene algebra terms equivalence in Coq
- Automated reasoning and mathematics. Essays in memory of William W. McCune
- Second-order properties of undirected graphs
- Commutative idempotent groupoids and the constraint satisfaction problem.
- Symmetric implication zroupoids and identities of Bol-Moufang type
- Revisiting MU puzzle: a case study in finite countermodels verification
- A Wos Challenge Met
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- 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
- Pascal's theorem in real projective plane
- Ehresmann theory and partition monoids
- THE MOUFANG LAWS, GLOBAL AND LOCAL
- Shortest single axioms for commutative Moufang loops of exponent 3.
- Treewidth-two graphs as a free algebra
- Directly indecomposables in semidegenerate varieties of connected po-groupoids
- Lattice theory for rough sets -- a case study with Mizar
- Automatically Proving and Disproving Feasibility Conditions
- mu-term: Verify Termination Properties Automatically (System Description)
- Tactics and certificates in Meta Dedukti
- Old or heavy? Decaying gracefully with age/weight shapes
- Right-orderability versus left-orderability for monoids
- Foundations of coloring algebra with consequences for feature-oriented programming
- Model finding for recursive functions in SMT
- On weakly associative lattices and near lattices
- Use of logical models for proving infeasibility in term rewriting
- Automatic generation of logical models with AGES
- Generalised domain and \(E\)-inverse semigroups
- Transitive Separation Logic
- Foundations of concurrent Kleene algebra
- Permutation of elements in double semigroups
- Modal algebra and Petri nets
- nanoCoP: a non-clausal connection prover
- Relational lattices via duality
- SETHEO
- RegStab
- RelView
- Alloy
- LOOPS
- OTTER
- Darwin
- SPASS
- FINDER
- E-Darvin
- Mace4
- AURA
- Kodkod
- E-SETHEO
- ProB
- LOOPS
- RiG
- ARA
- KAT-ML
- Ralf
- RALL
- CERES
- Tipi
- Equinox
- iProver
- leanCoP
- JProver
- Saigawa
- FAdo
This page was built for software: Prover9
