Timeline

Not logged in

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

50 descendants and 50 ancestors of [207908bad1]

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
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