inductive vs equational definition and theorems

[partizanos]

i dont get differnece in inductive and equational proofs: they both have the same theorems inductive reflexivity: Reflexivity : ∀t ∈ TΣ,s ,t = t ∈ ThInd (Spec) equational reflexivity: Reflexivity : ∀t ∈ TΣ,s ,t = t ∈ Th(Spec) i dont get the difference: ThInd (Spec) and Th(Spec)

[partizanos]

only the cut therem is different i think it is the essence of the deduction that permits as to prove something from the Theorems, based on the "enchanced" cut on induction theorems But I am not sure.. I speak for the ADT slide 40

[partizanos]

There is a remark in slide 39 mentioning the following but it is not so clear to me. Remark : Th(Spec) ⊆ ThInd (Spec) and the induction rule define the inductive theories.

[didierbuchs]

The main diff?rence is the induction rule that says that proving P(x) for any t/x then the Formula \forall x, (P(x) is valid. It means that we can synthetize universally quantified variables from proof on specific values.

The rest of the axioms are the same obviously because they reflect properties of equality or functions.

Envoy? de mon iPad

Le 28 janv. 2018 ? 16:56, Dimitrios Proios notifications@github.com<mailto:notifications@github.com> a ?crit :

i dont get differnece in inductive and equational proofs: they both have the same theorems inductive reflexivity: Reflexivity : ?t ? T?,s ,t = t ? ThInd (Spec) equational reflexivity: Reflexivity : ?t ? T?,s ,t = t ? Th(Spec) i dont get the difference: ThInd (Spec) and Th(Spec)

- You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/cui-unige/modelisation-verification/issues/19, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AF8XGXMWtEzmvFe2Wsg55kqad952Vksmks5tPJi4gaJpZM4RvvnV.

{"api_version":"1.0","publisher":{"api_key":"05dde50f1d1a384dd78767c55493e4bb","name":"GitHub"},"entity":{"external_key":"github/cui-unige/modelisation-verification","title":"cui-unige/modelisation-verification","subtitle":"GitHub repository","main_image_url":"https://cloud.githubusercontent.com/assets/143418/17495839/a5054eac-5d88-11e6-95fc-7290892c7bb5.png","avatar_image_url":"https://cloud.githubusercontent.com/assets/143418/15842166/7c72db34-2c0b-11e6-9aed-b52498112777.png","action":{"name":"Open in GitHub","url":"https://github.com/cui-unige/modelisation-verification"}},"updates":{"snippets":[{"icon":"DESCRIPTION","message":"inductive vs equational definition and theorems (#19)"}],"action":{"name":"View Issue","url":"https://github.com/cui-unige/modelisation-verification/issues/19"}}}

[didierbuchs]

In fact the cut is just here for the conditional axioms.

Envoy? de mon iPad

Le 28 janv. 2018 ? 17:04, Dimitrios Proios notifications@github.com<mailto:notifications@github.com> a ?crit :

only the cut therem is different i think it is the essence of the deduction that permits as to prove something from the Theorems, based on the "enchanced" cut on induction theorems But I am not sure.. I speak for the ADT slide 40

- You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/cui-unige/modelisation-verification/issues/19#issuecomment-361073710, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AF8XGWzD7zmg9pRGhIUoVoy-5aG7bU95ks5tPJqTgaJpZM4RvvnV.

{"api_version":"1.0","publisher":{"api_key":"05dde50f1d1a384dd78767c55493e4bb","name":"GitHub"},"entity":{"external_key":"github/cui-unige/modelisation-verification","title":"cui-unige/modelisation-verification","subtitle":"GitHub repository","main_image_url":"https://cloud.githubusercontent.com/assets/143418/17495839/a5054eac-5d88-11e6-95fc-7290892c7bb5.png","avatar_image_url":"https://cloud.githubusercontent.com/assets/143418/15842166/7c72db34-2c0b-11e6-9aed-b52498112777.png","action":{"name":"Open in GitHub","url":"https://github.com/cui-unige/modelisation-verification"}},"updates":{"snippets":[{"icon":"PERSON","message":"@partizanos in #19: only the cut therem is different i think it is the essence of the deduction that permits as to prove something from the Theorems, based on the \"enchanced\" cut on induction theorems \r\nBut I am not sure.. I speak for the ADT slide 40\r\n"}],"action":{"name":"View Issue","url":"https://github.com/cui-unige/modelisation-verification/issues/19#issuecomment-361073710"}}}

[didierbuchs]

This inclusion assert that there are more theorems that we can deduce with the inductive theories, those that are defined with universal quantification that cannot be Obtained with equational theories. This is the case for instance with commutativity In natural specificationn or with not(not(x))=x . It is not strictly greater because in some Very specific cases inductive and equationbal theories can coincide.

Envoy? de mon iPad

Le 28 janv. 2018 ? 17:16, Dimitrios Proios notifications@github.com<mailto:notifications@github.com> a ?crit :

There is a remark in slide 39 mentioning the following but it is not so clear to me. Remark : Th(Spec) ? ThInd (Spec) and the induction rule define the inductive theories.

- You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/cui-unige/modelisation-verification/issues/19#issuecomment-361074462, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AF8XGS2XEl_svlDoTfJPcAqDKdp5nuOJks5tPJ00gaJpZM4RvvnV.

{"api_version":"1.0","publisher":{"api_key":"05dde50f1d1a384dd78767c55493e4bb","name":"GitHub"},"entity":{"external_key":"github/cui-unige/modelisation-verification","title":"cui-unige/modelisation-verification","subtitle":"GitHub repository","main_image_url":"https://cloud.githubusercontent.com/assets/143418/17495839/a5054eac-5d88-11e6-95fc-7290892c7bb5.png","avatar_image_url":"https://cloud.githubusercontent.com/assets/143418/15842166/7c72db34-2c0b-11e6-9aed-b52498112777.png","action":{"name":"Open in GitHub","url":"https://github.com/cui-unige/modelisation-verification"}},"updates":{"snippets":[{"icon":"PERSON","message":"@partizanos in #19: There is a remark in slide 39 mentioning the following but it is not so clear to me.\r\nRemark : Th(Spec) ? ThInd (Spec) and the induction rule define\r\nthe inductive theories.\r\n"}],"action":{"name":"View Issue","url":"https://github.com/cui-unige/modelisation-verification/issues/19#issuecomment-361074462"}}}

[partizanos]

Thank you a lot for your answers.

Mini-questions: 1.(P=stands for proof? , t/x stands for combinations of terms and variables?)

2.how can i read this:

3. proving P(x) for any "t/x", what is the "t/x" ?? (My guess: if all variables and terms are able to "replace the parameters"" in the equation (or proof?) Px)

4.P(x)is valid means P(x)= True?

[didierbuchs]

On 29 Jan 2018, at 03:47, Dimitrios Proios notifications@github.com<mailto:notifications@github.com> wrote:

Thank you a lot for your answers.

Mini-questions: 1.(P=stands for proof? , t/x stands for combinations of terms and variables?)

P stands for a predicate, it is parameterised suc as P(x)=x>0 or x<=0

2.how can i read this:

1. proving P(x) for any "t/x", what is the "t/x" ?? (My guess: if all variables and terms are able to "replace the parameters"" in the equation (or proof?) Px)

you are right, x is a variable so t is a value that can replace it, P(x)[x/3], in our case it means P(3)=3>0 or 3<=0

4.P(x)is valid means P(x)= True?

sort of, but a predicate is not a function, it is a relation.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/cui-unige/modelisation-verification/issues/19#issuecomment-361125816, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AF8XGW6aMTevYh-O1_5SxahKjUjfjMggks5tPTE8gaJpZM4RvvnV.

{"api_version":"1.0","publisher":{"api_key":"05dde50f1d1a384dd78767c55493e4bb","name":"GitHub"},"entity":{"external_key":"github/cui-unige/modelisation-verification","title":"cui-unige/modelisation-verification","subtitle":"GitHub repository","main_image_url":"https://cloud.githubusercontent.com/assets/143418/17495839/a5054eac-5d88-11e6-95fc-7290892c7bb5.png","avatar_image_url":"https://cloud.githubusercontent.com/assets/143418/15842166/7c72db34-2c0b-11e6-9aed-b52498112777.png","action":{"name":"Open in GitHub","url":"https://github.com/cui-unige/modelisation-verification"}},"updates":{"snippets":[{"icon":"PERSON","message":"@partizanos in #19: Thank you a lot for your answers.\r\n\r\nMini-questions:\r\n1.(P=stands for proof? , t/x stands for combinations of terms and variables?) \r\n\r\n2.how can i read this:\r\n\r\n3. proving P(x) for any \"t/x\", what is the \"t/x\" ?? \r\n (My guess: if all variables and terms are able to\r\n\"replace the parameters\"\" in the equation (or proof?) Px)\r\n\r\n4.P(x)is valid means P(x)= True? "}],"action":{"name":"View Issue","url":"https://github.com/cui-unige/modelisation-verification/issues/19#issuecomment-361125816"}}}