Open saucisson opened 6 years ago
Hello, I am not sure what is expected to write in the TODO of proof_spec.lua file, could you explain it a bit more analytically? Any hints?
In proof_spec.lua
, you have to fill the proof that x+y = y+x
, using the constructs that have been defined in theorem.lua
. You can look at proofs that have already been done in theorem_spec.lua
.
In the transitivity method, in the code, there is a line:
local ok, variables = Adt.Term.equivalence (lhs [2], rhs [1])
. . . which gives ok the value of true if lhs[2] and rhs[1] are equal to each other.
This represents the acknowledgement that in t=tAND t
=t`, the second term of the left-hand side (t
in this case) and the first term of right-hand side(tin this case) are equivalent. This needs to be so in order for transitivity to be applied. However, substitutivity has no such conditions - there are many AND gates, and they are not dependent on each other - t must be equal to t
, but that is within the clause. There is no relationship between t(n) and t(n+1), for example. The terms between the clauses are independent. So how are we supposed to obtain the variables that are mentioned in the end of the method? Thanks.
You have to ask yourself: what is the purpose of the variables
field, that is returned by every Theorem.*
function?
Question how can we access from in a theorem such as s(0) + x = s(x) lets assume it is t1 to apply substitution on the s(x) to make it s(x+0) how can we send the variable?
--Trying to substitute:
Theorem.substitution(
t1,
t1.variables [Natural.Successor{Natural._x}],
Natural.Addition { Natural._x, Natural.Zero {} }
)
--This return value
t1.variables [Natural._x]
--This return nill
t1.variables [Natural.Successor[Natural._x]]
I know it is late just curious...
And second question the required packages such as adt where are they in the filesystem? I could not find them within the project folder :/
The art
module is in modelisation-verification/homework/proofs/src/adt/init.lua
. You have to run the luacheck
, busted
, .... commands within modelisation-verification/homework/proofs/
, and they should automatically find the modules.
I wanted to see its inner implementation mostly, busted and luacheck run good indeed :)
Hello I want to ask if the homework 3 was corrected because in the TP of Friday it was mentioned it would be release in some hours but I have not yet received a correction and I am not sure if it is because my github repo has some problem or because it was not yet released. Thank you in advance
Sorry, grades will be pushed in a few days.
Homework #3 has been released. Deadline is 15 november 2017 at 23:59. Look at the course homepage for more information.