Prover9

Prover9 and Mace4: Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 197 articles )

Showing results 1 to 20 of 197.
Sorted by year (citations)

1 2 3 ... 8 9 10 next

  1. Aceto, Luca; Castiglioni, Valentina; Ingólfsdóttir, Anna; Luttik, Bas; Pedersen, Mathias Ruggaard: On the axiomatisability of parallel composition (2022)
  2. Stokes, Tim: ((\mathscrF,\mathscrG))-abundant semigroups (2022)
  3. Abbadini, Marco: Equivalence à la Mundici for commutative lattice-ordered monoids (2021)
  4. Araújo, Maria Leonor; Araújo, Maria Teresa; Kinyon, Michael: The solution of an open problem on semigroup inclusion classes (2021)
  5. Bergstra, Jan A.; Ponse, Alban; Staudt, Daan J. C.: Non-commutative propositional logic with short-circuit evaluation (2021)
  6. Coghetto, Roland: Pappus’s hexagon theorem in real projective plane (2021)
  7. Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: Semidistributivity and whitman property in implication zroupoids (2021)
  8. East, James; Gray, Robert D.: Ehresmann theory and partition monoids (2021)
  9. Jackson, Marcel; Stokes, Tim: Override and update (2021)
  10. Jipsen, Peter; Tuyt, Olim; Valota, Diego: The structure of finite commutative idempotent involutive residuated lattices (2021)
  11. Macke, Jaroslav; Sedlar, Jiri; Olsak, Miroslav; Urban, Josef; Sivic, Josef: Learning to solve geometric construction problems from images (2021)
  12. Margolis, Stuart; Stein, Itamar: Ehresmann semigroups whose categories are EI and their representation theory (2021)
  13. Merlini Giuliani, Maria de Lourdes; Oliveira Cortes, Wagner de: On loopoids and magma with inverse (2021)
  14. Santocanale, Luigi: Dualizing sup-preserving endomaps of a complete lattice (2021)
  15. Sawicki, Damian; Grabowski, Adam: On weakly associative lattices and near lattices (2021)
  16. Wehrung, Friedrich: Right-orderability versus left-orderability for monoids (2021)
  17. Wernhard, Christoph: Craig interpolation with clausal first-order tableaux (2021)
  18. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  19. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  20. Didurik, Natalia; Shcherbacov, Victor: Units in quasigroups with classical Bol-Moufang type identities. (2020)

1 2 3 ... 8 9 10 next