Algebraic Reasoning with Prover9
This page provides a link to a basic proof
database, maintained by Peter Höfner, that contains the
Prover9
input and output files of proof experiments with
- idempotent semirings and Kleene algebras,
- idempotent semirings and Kleene algebras with tests,
- modal semirings and modal Kleene algebras,
- omega algebras (with tests),
- demonic refinement algebras,
- boolean algebras with operators,
- relation algebras.
Prover9 is a
resolution- and paramodulation-based automated theorem prover
developed by William
McCune.
If you want to contribute to the proof database, please send us your
input files and any information that will help us to replay your
proofs.
An Isabelle
repository for relational and algebraic methods can be found
via this link.