Timeline

Not logged in

 2015-04-15 14:32 Fixed module declarations/imports for the new argument pattern for elaborate. check-in: 207908bad1 user: andy tags: trunk 14:31 Fixed a small logical mistake in a footnote. check-in: 556662b818 user: andy tags: trunk 11:48 Added some extra arguments to the premise/conclusion hooks: index (for antecedants), path, and the actual term itself. check-in: f84190c56c user: andy tags: trunk 11:47 Split the What argument to elaborate into What and Data. What is now either 'goal' or 'ctx', while data identifies the sub-element. For ctx this is the index, but it can also be the index of a disjunct (when the goal is a disjunction), or 'ih' to indicate backchaining the user goal on the IH instead of on its definitions. check-in: 9e954b6b56 user: andy tags: trunk 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 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