We have built a basic proof database, 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.
We thank B. Möller, G. Schmidt and G. Struth for their contribution and their support.
 

Furthermore, we have generated a library of small models with Mace4 for

• idempotent semirings (with tests),
• Kleene algebras (with tests),

Mace4 searches for finite structures satisfying first-order and equational statements, the same kind of statement that Prover9 accepts. it is also developed by William McCune.
 

For some paper we provide special data. Click at the title to access the data.

• P. Höfner, B. Möller: An Extension for Feature Algebra
  
  
• P. Höfner: Algebraic Calculi for Hybrid Systems (PhD thesis) .
  
  
• P. Höfner, G. Struth, G. Sutcliffe: Automated Verification of Refinement Laws. (to appear).
  
  
• H.-H. Dang, P. Höfner: First-Order Theorem Prover Evaluation w.r.t. Relation- and Kleene Algebra. In R. Berghammer, B. Möller, G. Struth (Eds.): RelMiCS/AKA >PhD programme, Technical Report 2008-04, Universität Augsburg, pp.48-52, 2008).
  
  
• P. Höfner: Automated Reasoning for Hybrid Systems --- Two Case Studies ---. In R. Berghammer, B. Möller, G. Struth (Eds.): RelMiCS/AKA 2008, Lecture Notes in Computer Science 4988, Springer, pp.191-205, 2008.
  
  

• Supported Internet Browser
  The proof database uses JavaScript and MATHML, which are nowadays standard. As far as we know all common browsers like Firefox, Mozilla, Opera and Iceweasel work well. Only Iceweasel has still some problems when displaying MATHML, but the outcome is readable.
  The Internet Explorer does not support the MATHML-standard. To get nice mathematical output one has to install MathPlayer.
  If some pages are empty, you propably disabled Java Script.
• Feedback
  Feedback will be appreciated. Please send any kind of comments to Peter Höfner.