Timeline

Not logged in

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

50 most recent timeline items

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