-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Put all progress reports in one place on master
- Loading branch information
1 parent
ac7ddf4
commit b56f88c
Showing
4 changed files
with
21 additions
and
0 deletions.
There are no files selected for viewing
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
Changelog for jkstpierre: | ||
|
||
11/20/2018: | ||
- Proved with Professor Dougherty that substitutions | ||
distribute. This was the final link required for | ||
connecting the fundamental idea behind unification, | ||
namely that "sigma" being a unifier for terms "t1, t2" | ||
if (sigma t1) = (sigma t2) is equivalent to saying | ||
(sigma t) = 0 for some term t. | ||
- Wrote functions for evaluating ground terms to 0 or 1. | ||
- Wrote definition for a more general substitution. | ||
- Wrote definition for a most general unifier. | ||
- Proved an example from the book for being a most | ||
general unifier. | ||
- Wrote preliminary definitions for Lowenheim's formula. | ||
- Wrote auxilliary helpers for variable membership in | ||
terms. | ||
|
||
11/21/2018: | ||
- Wrote some tentative examples for Lowenheim's formula | ||
checking to see if it is generating mgu's. |
File renamed without changes.
File renamed without changes.