Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
50 most recent check-ins
|
2023-01-25
| ||
| 09:24 | Fixed a missing script import in the REPL example. Leaf check-in: b8ed293298 user: andy tags: trunk | |
|
2015-05-07
| ||
| 09:54 | Updated presentation: final version. 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 | |