Timeline

Not logged in

 2015-05-07 09:54 Updated presentation: final version. Leaf check-in: a01b5086af user: andy tags: trunk 2015-05-01 09:12 Added an index page to the server, so you can browse http://localhost:4001 and get nice links to the examples. check-in: 3bb6b9ecdb user: andy tags: trunk 2015-04-30 07:06 Updated flyer with presentation location. check-in: 855f5cd0f0 user: andy tags: trunk 2015-04-28 21:18 Fixed some typos. check-in: 71edd53195 user: andy tags: trunk 21:13 Added presentation flyer files. check-in: c387492ea6 user: andy tags: trunk 2015-04-27 12:59 Just making sure the poster was up-to-date. check-in: 6466816782 user: andy tags: trunk 2015-04-26 21:15 Full presentation (still draft). check-in: dab782646e user: andy tags: trunk 16:27 Fixed a missing section reference. check-in: e4688d49fd user: andy tags: trunk 16:26 Fixed a typo in the poster. check-in: b0f1fc67b4 user: andy tags: trunk 2015-04-23 16:08 Finished poster. check-in: 8547fc1005 user: andy tags: trunk 2015-04-22 20:50 Presentation work. check-in: 1275718981 user: andy tags: trunk 20:50 Added jsonterm module, eventually to replace term_to_json (which is terrible). check-in: 0784891462 user: andy tags: trunk 20:50 Commented out tentative section of universal/existential quantification. check-in: c98b0d6d4e user: andy tags: trunk 20:49 Added poster for appreciation reception. check-in: 8078001da1 user: andy tags: trunk 10:30 Added material to the report on the handling of explicit quantifiers. Leaf check-in: 8a438a8abd user: andy tags: forall-exists 10:29 Presentation work. Added PDF of presentation. Leaf check-in: a24ff57f47 user: andy tags: trunk 2015-04-21 21:35 Started work on better handling of forall/exists in the reasoning language. Leaf check-in: e8532f2591 user: andy tags: forall-exists 19:26 The new clausal-expansion system for goals is complete. Closed-Leaf check-in: d8a8e82a90 user: andy tags: bc-subst 16:26 Added reference to Gacek's PhD thesis in the section on induction. Added screenshot of a completed proof. check-in: ec0abfb8eb user: andy tags: bc-subst 16:25 Removed hover styles from premise/conclusion classes (this should be handled in JS, so that it can be disabled when the proof is complete). check-in: 6feebbe110 user: andy tags: bc-subst 16:25 Added proof demo example. check-in: 018383954d user: andy tags: bc-subst 15:47 Fixed everything else to work with the new goal/clausal expansion. check-in: 52b0f899a0 user: andy tags: bc-subst, working 15:47 Fixed module imports to avoid a (meaningless) warning. check-in: 8ad421112c user: andy tags: bc-subst 15:47 Fixed client-side proof handling to work with the new backchain fomat. check-in: 626e89a1ac user: andy tags: bc-subst 15:46 Added support for showing rule names in derivations. check-in: a989ccc9e5 user: andy tags: bc-subst 15:45 Fixed a bug in the translation of Uppercase atoms from Prolog. check-in: 223107a48f user: andy tags: bc-subst 2015-04-20 20:58 Updated checker module to work with the new atomic goal expansions. check-in: 4e6407ce10 user: andy tags: bc-subst 20:57 Fixed (maybe) the filtering of substitutions for "interesting" variables. check-in: abb4d08745 user: andy tags: bc-subst 09:54 Started work on making backchaining of goals a) apply the substitution to the expansion, rather than appending it as a conjunction of unifications, b) return the substitution along with each branch of the expansion, and c), return the name of the branch that was chosen (analogous to the index N parameter in choice proofs). check-in: 1252a63f55 user: andy tags: bc-subst 09:52 Fixed a minor typo. Leaf check-in: adaef9d668 user: andy tags: trunk 2015-04-18 21:14 Final draft of report. (Unless I think of something else to add...) check-in: 04f1cd0696 user: andy tags: trunk 19:48 Penultimate draft of the report. After spell checking and such, this will become the final draft. check-in: 98924328ad user: andy tags: trunk 18:47 Added a TODO comment describing the problems around applying the substitution to the body of an expanded clause, instead of appending them as unification goals. check-in: b5c5523821 user: andy tags: trunk 18:46 Fixed tests to support the new definition of atoms (can be constructed from numbers). check-in: 51ec69316b user: andy tags: trunk 18:45 Added an exposed predicate for checking proofs (just checking, no elaboration). check-in: b1dff5705c user: andy tags: trunk 18:45 Fixed a bug in the checker, context was not being initialized to [] which made goals succeed once and then enter an infinite loop. check-in: f931058aa9 user: andy tags: trunk 16:44 Fixed a bug in proofs that involve backchaining on the IH. check-in: c4c963bcde user: andy tags: trunk 16:44 Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate. check-in: 95a716e7e5 user: andy tags: trunk 2015-04-16 22:02 Fixed many small bugs in elaboration, checking of incomplete proofs. check-in: 6ca1a452f3 user: andy tags: trunk 22:01 Fixed demo IH to conform to the new vertical-bar encoding. check-in: 925c93ea0a user: andy tags: trunk 22:00 Fixed a bug in merging of substitutions with some arguments unbound. check-in: acfcbdeb7a user: andy tags: trunk 21:59 Fixed a bug in fill that was duplicating _'s in the to-be-copied term. check-in: a992c2ca2e user: andy tags: trunk 21:59 Fixed a few bugs in rendering of proofs (commas between antecedants, tabindexes on conclusions so they can be keyboard-focused). check-in: 5ae5431e8f user: andy tags: trunk 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 21:36 Changed the encoding for inductive goals from \size to |size. The backslash was getting lost in the string encoding in some places. check-in: 23db977deb user: andy tags: trunk 20:17 Added a new "PVar" subtype of Term, for Prolog variables that need to be preserved as such (i.e., distinguished from specification variables). check-in: 8949a9e372 user: andy tags: trunk 19:51 Fixed a bug in the conversion to Prolog of numeric atoms (0 vs. '0'). check-in: 76226466c7 user: andy tags: trunk 19:43 Fixed a couple bugs in the handling of non-string atoms (coerce to string). check-in: 808229ea10 user: andy tags: trunk 19:42 Fixed a bug in case analysis of atomic goals. check-in: afb3b37674 user: andy tags: trunk 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