-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsantonatos.txt
159 lines (98 loc) · 6.55 KB
/
santonatos.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
For Monday 1/28:
Things I worked on:
- modified the definition of var_set_create_unique to make it more efficient and clean and proved lemmas for it
like distribution.
- completed the core proof (book's proof for the builder):
+ using classical logic, proved mgu for all x, filling in any important admitted lemmas related to it (2-3)
+ filled in a lot of small helper admitted lemmas used for the proof (4-5) and added and proved
more used for these (another 4-5) (made the proof for unique vars, not only vars)
Things to work on:
- start working on the extension of the proof for the main function
For Monday 1/21:
Things I worked on:
- made a draft extension of the mgu proof to include the Main Lowenheim's function.
- proved an important helper lemma for the "reproductive proof" of the builder, which is
that applying lowenheim's substitution on a variable gives us the initial format of the replacement.
Plans:
- finish the helper lemmas for the lownheim_builder mgu proof.
- cut from the proof the case for which x is not in Var(t)
-----------------------------------------------------------------------------
During Christmas break :
Things I worked on:
- changed the format of our lowenheim builder to math the format of lemma 10.4.5
- proved lemma 10.4.5 and then that our lowenheim builder unifies , having added 3 admitted helper lemmas
- added property for rewrites within apply_subst, having added 1 admitted helper lemma
- proved that our lowenheim builder gives a substitution that is reproductive, having added 2 admitted helper lemmas
- proved that any reproductive unifier is also a most general unifier
- proved that our lowenheim builder gives a most general unifier
- fixed our apply_subst function to account for replacements that refer to each other (so that they do not get mixed up)
and modifierd (reproved) all the lemmas that were already proved and involved apply_subst
Plans:
- reorganize the files by splitting our terms.v files
- clean up our existing files by removing unused coq code and developement
- add more writing
- start filling in helper admitted leamms
----------------------------------------------------------------------------------------------------------------
For Thursday 12/13 :
Things I worked on:
- added introductory subsections to the intro chapter of the report
- worked on 10.4.5 , but after failing to keep the current format and solve the existing problem
by adding the extra l, decided to try a new apporach by changing how the lemma is formed, but that still in the works
(adding a list of vars and changing the proposition equivalence to a list of replacements) - more like professor's version
. Still admitted though and working on it.
-finally merged lowenheim_dev with the rest of the team.
Plans/ problems
- finish 10.4.5 !!!
- finish the other two proofs based on 10.4.5 (one of them is done but if 10.4.5 's format changes, it needs to change too)
------------------------------------------------------------------------------------------------------
For Monday 12 / 9 :
Things I worked on:
- added a correction on Lowenheim main formula. Added testing for find_ground_unifier function.
- imporved a lot the proof. Multiple attempts to prove 10.4.5, proved that lowenheim unifies based on admitted 10.4.5
- added some documentation
Problems /plans:
- no universal way to check the correctness of the output of Lownheim's function, have to prove the equivalence with axioms manually, after the sunstitution
- stuck on an induction step for the proof of 10.4.5
- 1 proof left : lowenheim is a reproductive unifier.
---------------------------------------
For Thursday 12 / 6:
Things I worked on:
- Completed and cleaned Lowenheim's algorithms, by improving existing main function, creating more helper functions
and introducing new data type subst_option
- Added small sentences / paragraphs as part of the report withing the source files. All functions/definitions are documented/commented
and all subsections are created.
- Created without proving 2 Lemmas from the book, necessary for proving Lowenheim's formula
Problems / Plans:
- verify correctness of Lemmas and start on the proof
- more on the report commenting && pdf generation
-------------------------------------------------------------
For Monday 12 / 3 :
Things I worked on :
- completed Lowenheims main formula / function
- worked with Joseph to slightly tweak definitions of more general unifiers and most general unifiers, added reproductive unifier definition.
- added new versions of term evaluation / simplification functions that helped to define the main Lowenheim formula
Problems / plans :
- still a bit unclear path about the proof. Perhaps the use of reproductive unifier would help? further focus / consultation on the proof now that most/all of Lowenheim formulation is complete
- some issues with rewrites with the "==" equivalence symbol, cannot rewrite within context of other function, to use ub the proofs if simple examples.
--------------------------------------------------------------
for Thursday 11/29:
things I am working on and will be working on this week:
- developing the feauture that lowenheim finds the ground solutions on its own.
Having some trouble finding a way to produce all the possible combinations (subsets )
of a list of vars, perhaps using the permutation coq library?
- refactoring the code to eqv from equal. After replacing the definitions with eqv and using prof's Dougherty
helper definitions / additions, there are issues with some of the proofs. Complex examples do not work as before, they require special
changes , as well as some of the proofs. The usual error that comes up is that "eqv" is not "Proper" inside the error message. Joseph said he fixed the above by adding two
more axioms and he will talk with the professor about them; awaiting further counseling on this.
------------------------------------------------------------------
for Tuesday 11/27:
things I worked on last week:
- the evaluation function for simplifying terms made of 0's and 1's,
e.g. the multipliation and the addition function
- adding feautres to Lowenheim's base formula, the check_correct input function
and the ability of the function to take multiple ground solutions and produce multiple unifiers
Problems and things to work on:
- github problem, I am kind of stuck on a branch I pulled and I have tried several ways to undo it, but it's hard
- add more example with lowenheim's new formula
- potential feauture, lowenheim finds its ground solutions by itself
- look more into the proof, the definition of mgu and "more general unfier"