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)
- Automated Reasoning in Kleene Algebra
- Herbrand constructivization for automated intuitionistic theorem proving
- Automatic generation of logical models with AGES
- Permutation of elements in double semigroups
- Minimal paths in the commuting graphs of semigroups
- Order in implication zroupoids
- Developments in concurrent Kleene algebra
- A note on regular De Morgan semi-Heyting algebras
- Algebraic separation logic
- Concurrent Kleene algebra and its foundations
- Internal axioms for domain semirings
- On hom-algebras with surjective twisting
- Expansions of semi-Heyting algebras. I: Discriminator varieties
- Automated verification of refinement laws
- A natural characterization of semilattices of rectangular bands and groups of exponent two.
- SPASS
- FINDER
- E-Darvin
- Mace4
- AURA
- Kodkod
- E-SETHEO
- ProB
- Type-2 fuzzy sets and bichains
- Generalised domain and \(E\)-inverse semigroups
- LOOPS
- RiG
- ARA
- KAT-ML
- Ralf
- RALL
- CERES
- Tipi
- Equinox
- iProver
- leanCoP
- JProver
- Saigawa
- FAdo
- GUItar
- PDCoq
- Prefuse
- tptp2X
- MaGIC
- Semigroups
- Conditional Confluence
- PTSC
- EQP
- Magma
- DISCOUNT
- Waldmeister
- Shred
- IDV
- ConCon
- ModGen
- OTT2MIZ
- GAPT
- ProofTool
- InKreSAT
- Peers-mcd
- Tribe
- Scavenger
- CO3
- ENIGMA
- FORT
- Meta Dedukti
- Stone Algebras
- Twee
- FLOTTER
- UACalc
- AGES
- BDDTab
- CoDe
- KAD
- infChecker
- GKC
- Relation Algebra
- DLPEQ
- TreeRePair
- Tarskis_Geometry
- lpeq
- Slakje
- WhaleProver
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Foundations of concurrent Kleene algebra
- XPlain
- CompoSAT
- DynAlloy
- ProverX
- Relational lattices via duality
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Modal algebra and Petri nets
- Semisimple varieties of implication zroupoids
- Transitive Separation Logic
- ProofWatch: watchlist guidance for large theories in E
- nanoCoP: a non-clausal connection prover
- Concurrent Kleene Algebra
- Axiomatizing the skew Boolean propositional calculus
- Sublattices of associahedra and permutohedra
- The structure of finite commutative idempotent involutive residuated lattices
This page was built for software: Prover9
