Skip to content
Snippets Groups Projects
  • Released date
  • Created date

0.3

Evidence collection

0.3-evidences-173.json e9beccf2
Collected 2 years ago

Release notes

This release overhauls the entire document, but introduces only few changes to the proof format itself.

The standard now specifies that assume commands can only be issued at the start of the proof or right after an anchor command.

Beyond many smaller clarifications and typographic improvements, the following changes are implemented in this release.

  • Add an abstract proof checking procedure to clarify the semantics of the proof format.
  • Add a description of the semantics of contexts based on λ-terms.
  • List all transformations that are implicit in Alethe proofs.
  • Change the notation used for terms from first-order style (e.g., f(x, g(y))) to higher-order style (e.g., (f x (g y))). This is only a change in notation -- the used logic remains many-sorted first-order logic.
  • Eliminate the distinction between if-and-only-if and equality. Instead, use equality (the symbol ≈) with appropriate sorts.
  • Add an index that lists all proof rules.

Proof rules:

  • The rule implies_simplify is no longer allowed to perform the simplification (φ₁ → φ₂)→ φ₂ ⇒ φ₁ ∨ φ₂. This is now covered by bool_simplify.

0.2

Evidence collection

0.2-evidences-156.json 46827f20
Collected 2 years ago

Release notes

This is an intermediate release. It collects all changes to the original specification document before the major changes that were implemented as part of Hans-Jörg Schurr's PhD thesis. These changes will be reflected in release 0.3.

This release implements major changes to the structure of the document to clarify the difference between the language and the rules. The language has a formal definition and a proof of soundness. The syntax describes how proofs are encoded in the text file.

The syntax was extended to allow extra annotations. Tools consuming Alethe proofs must be able to ignore such extra annotations.

List of rules:

  • Improve description of sko_ex.
  • Add hole rule to allow holes. A proof that contains steps that use this rule is not valid.

Corrections:

  • Grammar: the choice binder can only bind one variable.

Clarifications:

  • Clarify functionality of choice in introduction.
  • Add illustrating example to introduction.
  • Normalize printing of (variable, term) arguments in the abstract notation.
  • Fix linear arithmetic example in introduction.
  • Change syntax of abstract proof steps to be clearer.