Check-in [e902cf4ec5]

Not logged in

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

Overview
Comment:Added some utilities for working with proof terms (extracting subproofs, getting proof goals, navigating through proofs on a path, etc.)
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:e902cf4ec544ddc283a1bee5e1c3ea599381ef22
User & Date: andy 2015-04-15 11:12:05
Context
2015-04-15
11:44
Added screen shot of the proof assistant, starting a proof. check-in: caa7fbdd73 user: andy tags: trunk
11:12
Added some utilities for working with proof terms (extracting subproofs, getting proof goals, navigating through proofs on a path, etc.) check-in: e902cf4ec5 user: andy tags: trunk
2015-04-14
21:05
Added support for rendering rule names next to rules (as table captions). Names are *not* rendered on rule applications in derivations, mostly because names are not stored in the proof tree. check-in: 0672529592 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to src/proof.js.

1
2
3
4
5
6

7
8
9
10
11


12

13
14

15
16
17


18
19
20
21
22
23
24
25
26
27





28





29
30
31
32
33
34



35



































/*
 * proof.js
 * Proof- (reasoning-) level routines.
 */

/* Proofs (in tandem with statements) are implemented within the Arend 

   resolution system as a kind of pseudo-module (the names of all predicates
   exported by the module are prefixed with \0 so that they cannot be accessed
   from "normal" specification code). The main predicate is

     verify(Statement,Derivation, Program)




   which succeeds if Deriviation is a proof of Statement in Program. Statements 
   are simply terms generated by the `statement` module, while deriviations are 

   terms compatible with those generated by the resolution procedure itself. A
   program is just a list of (normalized) definitions. (Various accessory 
   predicates allow "introspection" on programs.) 



   Inductive proofs rely on an extension to the resolution procedure that is 
   not used in normal programs: term "size" tracking. When a term has a .size
   attribute the resolution procedure will preserve the value of .size whenever
   that term is expanded as a predicate call. E.g., if we have the database

     foo(X) :- bar(X), baz.
     bar(_).
     baz.






   and the query






     foo#1(X).

   (where #1 gives the size of the term foo(X)) then the expansion will be

     bar#1(X), baz#1. 



*/








































<
>
|
<
<

<
>
>

>
|
<
>
|
|
|
>
>
|
<
<
<
<

<
<
<

>
>
>
>
>
|
>
>
>
>
>
|
<

<

<
>
>
>
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5

6
7


8

9
10
11
12
13

14
15
16
17
18
19
20




21



22
23
24
25
26
27
28
29
30
31
32
33
34

35

36

37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
/*
 * proof.js
 * Proof- (reasoning-) level routines.
 */



(function(proof){




var core = require('./core');
var terms = require('./terms');

/* proof.get(t,path)
 * Extract the subproof that is found by following a path.

 */
proof.get = function(t, path) {
    if(path.length === 0)
        return t;
    else
        return proof.get(proof.getSubProofs(t)[path[0]], path.slice[1]);
}









/* proof.getProofGoal(t)
 * Get the head of the goal of a proof. This will be something like
 *   = 
 *   and
 *   or 
 *   -> 
 *   true
 *   or a user goal.
 */
proof.getProofGoal = function(t) {
    return t.body[0].head;
}





/* proof.getSubProofs(t)
 * Get the JS array of subproofs from a given proof. Note that this is *child*
 * proofs, not descedants.
 */
proof.getSubProofs = function(t) {
    var proof = t.body[3];
    switch(proof.head) {
        // 0 subproofs
        case "trivial":
        case "hole":
        case "unify":
        case "ctxmem":
            return [];

        // 1 subproof, first argument
        case "ih":
        case "generic":
        case "implies":
        case "backchain":
            return [proof.body[0]];

        // 1 subproof, last argument
        case "induction":
        case "instan":
        case "choice":
            return [proof.body[proof.body.length-1]];

        // Product
        case "product":
            return terms.toArray(proof.body[0]);
    }

    // The only other option is case, which always has a list of
    // subproofs (0,1, or N elements):
    return terms.toArray(proofs.body[3]);
}


}(typeof exports === 'undefined' ? (this['arend']['proof'] = {}) : exports));