Timeline

Not logged in

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

50 ancestors of [0672529592]

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
20:49
Added support for rendering inductive goals with the up/down arrows. check-in: 98ef3fd317 user: andy tags: trunk
20:21
Added a specialized version of the nat specification, for demonstration purposes. check-in: 4a035bbfc0 user: andy tags: trunk
20:21
Added `passist` Pengine application to the server. This runs the live demo of the proof assistant. check-in: 3a093317cf user: andy tags: trunk
20:19
Changed the way the induction tactic handles repeated use (previous IHs are just ignored). check-in: c82ab7e9b6 user: andy tags: trunk
14:01
Added screenshot of the REPL UI. check-in: 2656521773 user: andy tags: trunk
14:00
Latest build results. check-in: b0c341eb78 user: andy tags: trunk
14:00
Better rendering of goals vs. terms. Subgoals of AND, OR, and IMP are now rendered as goals rather than terms. check-in: 8cf949cd23 user: andy tags: trunk
13:51
The REPL example now uses the client-side parser to check inputs for syntactical correctness. check-in: 0ce4e1a109 user: andy tags: trunk
13:50
Fixed a couple other bugs related to atoms-as-compounds. Changed the definition of symbolic tokens to *not* include commas, as it was misparsing things like `a,` as a single token. check-in: 5423c478ca user: andy tags: trunk
12:55
Fixed a bug in the prototype chain for Terms, added a term equality function. check-in: 0ae8435916 user: andy tags: trunk
12:55
Fixed an old but unnoticed bug in the parsing of termlists, introduced by the change from atoms being their own type to being 0-arity compounds. check-in: 27e97d3b88 user: andy tags: trunk
12:54
Additional styles for rules, derivations (relying on the new classes in `term_render`). check-in: 526989d708 user: andy tags: trunk
12:53
Some fixes/enhancements to term rendering. Atomic goals are now rendered with a different class from ordinary (data) terms. check-in: 583a0a23d4 user: andy tags: trunk
12:41
Added a test function to the REPL to check the consistency of terms as they go from string to JS to Prolog to JSON and back to JS. check-in: 673de1680c user: andy tags: trunk
2015-04-13
22:11
Tweaks to rendering of rules (added customization classes, fixed bug in recursive rule rendering). check-in: cfcf37f414 user: andy tags: trunk
22:10
Fixed a couple bugs in the REPL (not printing unifiers). check-in: 06cbeda353 user: andy tags: trunk
21:53
Major section reorganization. Hopefully things actually make sense now. check-in: 2af33ff4d5 user: andy tags: trunk
21:21
Finishing up related work section. Various minor cleanup, consistent terminology. check-in: 7f32fbc607 user: andy tags: trunk
20:39
Minor CSS adjustments. check-in: 4b35a7e91c user: andy tags: trunk
20:38
Added element test to nat specification. check-in: d3107f9d47 user: andy tags: trunk
2015-04-10
20:03
Added some details about the kinds of propositions, outside the specification logic, that the proof checker can prove. check-in: 3af3fa6bf3 user: andy tags: trunk
19:49
Updated references. check-in: 1a2bdba4bd user: andy tags: trunk
19:48
Added section on proof checking algorithm. check-in: aa430c5a51 user: andy tags: trunk
18:41
Added section of how the incremental proof checker works, including the elaboration rules. Moved some figures around. check-in: 8e35a0cc9b user: andy tags: trunk
18:40
Added `elaborate` for the elaboration (incremental construction) of partial proofs. Preliminary testing suggests that it seems to work. check-in: 2b98c54439 user: andy tags: trunk
18:40
Added export for `call_goal`. check-in: e53d599db5 user: andy tags: trunk
18:39
Added fill to exports; it was mistakenly omitted. check-in: 9ee7d84482 user: andy tags: trunk
08:15
A few comments and explanations. check-in: 39eb2a4b11 user: andy tags: trunk
2015-04-08
21:16
Fixed a minor spacing issue with citations. check-in: 3903630300 user: andy tags: trunk
21:13
Added support for printing MGUs (i.e., the actual solution you are looking for!) to the REPL. check-in: 754bdc3cbd user: andy tags: trunk
21:12
More report work (fleshed out preface). check-in: 9a2f6d91bf user: andy tags: trunk
14:00
Fixed a (dumb, obvious) bug in goal expansion normalization. check-in: d4d4b58a70 user: andy tags: trunk
14:00
Added a bit of code, preliminary to interactivity with proofs.    Removed dependency on MathJax. check-in: ee54c43f3a user: andy tags: trunk
13:59
Changed rendering to not use MathJax. Just wrap everything in styled spans. check-in: aa2ec6d43f user: andy tags: trunk
12:36
More work on rendering of derivations. check-in: 67dc3cf261 user: andy tags: trunk
12:36
Added the report PDF to the repo. check-in: b8d225937c user: andy tags: trunk
12:35
Additional work on the "future work" section. check-in: a7d8edc029 user: andy tags: trunk
2015-04-07
14:24
Added normalization/simplification of predicate call expansions, which should translate into simpler proofs/derivations. check-in: 3023e48bcb user: andy tags: trunk
12:58
Fixed a bug in substitution construction introduced by the previous fix. check-in: 5a1f522b34 user: andy tags: trunk
2015-04-06
10:43
Added another utility function to terms library. check-in: f8129ad438 user: andy tags: trunk
10:42
Further work on rendering proofs. check-in: ce8a8a63b5 user: andy tags: trunk
2015-04-04
20:52
Further work on rendering of derivations. Getting closer... check-in: 2611002f9f user: andy tags: trunk
20:52
Fixed a bug in the generation of nested proof objects. check-in: adcc6d5155 user: andy tags: trunk
2015-04-03
21:02
Rendering of terms and rules now works. The REPL example has been updated to download the full specification from the server and render it on page load.    Preliminary work on rendering derivations. check-in: aba371f926 user: andy tags: trunk
21:01
Fixed fromJSON so that Arend's logical variables are properly converted from atoms. check-in: 5b3a605fc4 user: andy tags: trunk
17:33
Changed program module to emit the same derivations as the full checker. check-in: f701cc9fad user: andy tags: trunk
16:45
Fixed `fromJSON` to work with Prolog's (undocumented) JSON term format. Fixed a few other things. check-in: c9cef7bdb8 user: andy tags: trunk
16:44
Made the Nat specification into a proper module. check-in: d3f15d45dc user: andy tags: trunk
16:44
Got the REPL example working. check-in: ad2e592612 user: andy tags: trunk
14:15
Added some utility routines to help passing terms to/from the PEngine backend. check-in: 1725103b73 user: andy tags: trunk