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

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)); |