Check-in [5f036d068a]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Updated to use the new inductive (vertical-bar) goal encoding.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:5f036d068af5bca445ac002183477808961da33b
User & Date: andy 2015-04-15 21:37:52
Context
2015-04-15
21:38
Fixed a bug in finding the subproofs of a case-type proof. check-in: f21f15e5e4 user: andy tags: trunk
21:37
Updated to use the new inductive (vertical-bar) goal encoding. check-in: 5f036d068a user: andy tags: trunk
21:37
Some additional styles for rendering of derivations. check-in: 9c0eace5aa user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to apps/passist/passist.pl.

22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
    term_to_json(Program,JSON).

% Initial proof state for the demo. This sets up the initial proof for the
% Goal with the induction done and ->R done. 
demo_proof(JSON) :-

    Proof = proof((nat(' x') -> add(' x', z, ' x')),[],_,
        induction(0,('nat\\sml'(' x')->add(' x', z, ' x')),
            proof(('nat\\big'(' x')->add(' x', z, ' x')),[],_,
                implies(proof(add(' x', z, ' x'),['nat\\big'(' x')],_,hole))))),

    term_to_json(Proof,JSON).

% check(Statement,Proof)
% Check the statement against the Proof
check(Statement,JSON) :-
    spec(Program),







|
|
|







22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
    term_to_json(Program,JSON).

% Initial proof state for the demo. This sets up the initial proof for the
% Goal with the induction done and ->R done. 
demo_proof(JSON) :-

    Proof = proof((nat(' x') -> add(' x', z, ' x')),[],_,
        induction(0,('nat|sml'(' x')->add(' x', z, ' x')),
            proof(('nat|big'(' x')->add(' x', z, ' x')),[],_,
                implies(proof(add(' x', z, ' x'),['nat|big'(' x')],_,hole))))),

    term_to_json(Proof,JSON).

% check(Statement,Proof)
% Check the statement against the Proof
check(Statement,JSON) :-
    spec(Program),