Logiweb(TM)

8.7.5 Proof checking

Prev Up Next Page 359 of 800 Search internet


The Logiweb proof checker verifies the proofs on a page as follows:

Finding the proofs on the page
The checker scans the codex for proofs. The codex contains definitions. A definition is a proof if it defines the proof aspect of a domestic construct. A construct is domestic if it is defined on the page itself. Non-domestic proofs are ignores so stating a proof on one page of a lemma from some other page has no effect.
Tactic expansion
Definitions are macro expanded before they reach the codex so the proof checker does not need to care about macro expansion. Instead, the proof checker does tactic expansion. It does so by doing normal evaluation (based on the value aspect) of the right hand side of each proof and then applying the result to the proof and to the cache of the page. The output of that is supposed to be a proof expressed in the Logiweb sequent calculus. If this process throws an exception, the proof is considered to be in error.
Sequent evaluation
The output from tactic expansion is sequent evaluated. For each proof this leads to a sequent of form << P ,, C ,, R >> where P is a set of premisses, C is a set of side conditions, and R is a result which holds if the given premisses and side conditions hold. If sequent evaluation throws an exception, the proof is considered to be in error.
Side condition check
The proof checker checks that C = {{}}. If not, the proof is considered to be in error.
Result check
As mentioned, a proof is a definition. The left hand side of the definition is the lemma which the proof is supposed to prove. The proof checker looks up the statement aspect of the lemma and compares that aspect to R. If they differ or if the statement aspect is undefined, the proof is considered to be in error.
Premise checking
For each premise in P, the proof checker verifies that the premise is a lemma which has been proved elsewhere. If the lemma belongs to the same page then the proof checker verifies that the lemmas do not use each other in a circular fashion. If the lemma belongs to some other page then the proof checker performs two checks. First, it looks up the diagnose hook of that other page to see that the other page is correct. Second, it looks up the claim aspect of the other page to see that the other page has been verified by the same proof checker.

Prev Up Next Page 359 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05