/*@ <webex id="firstOrderSyntax" type="riscal"
       header="Exercise: First Order Syntax" 
       href="http://fmv.jku.at/logik/index.html">
@*/
// ==============================================================
//
// firstOrderSyntax.txt
// An demonstration exercise in first order logic (syntax).
// (c) 2018, Project LogTechEdu, http://fmv.jku.at/logtechedu/
//
// This exercise consists of 4 tasks TASK 1-4 where each task
// consists of one ore more questions a,b,...
//
// This file is for demonstration; it provides both the questions 
// and corect answers to these questions. Study the questions, its
// answers, and run the checks of the correctness of the answers.
//
// ==============================================================

/*@
<display>
EXECUTION OPTIONS:
-----------------------------
</display>
@*/

//@ <option id="silent" label="Silent Execution:" type="bool">
/*@<display>
(set if you want to minimize output)

GENERAL:
-------------
The following definitions are used for the remainder of this exercise.
</display>@*/
//@ <public>
val N = 10;    // the maximum number in our domain
type D = ℕ[N]; // the domain of numbers 0..N
/*@ <display id="task1display">
Note that in the following checks, the requested syntactic properties of the
formulas that you enter will NOT be checked (only their equivalence to the given
formulas will be checked).

TASK 1 DESCRIPTION: 
-----------------------------
Below you see a formula F without parentheses:
</display>@*/
//@ <private>
pred p(x:D) ⇔ x > 0;
pred q(x:D) ⇔ x < N;
pred r(x:D) ⇔ x > 0 ∧ x < N;

pred withoutPar1(x:D) ⇔ 
//@ <public>
//@ <data id="task1data">
¬ p(x) ∧ q(x) ⇒ r(x)
//@ </data>
//@ <private>
;
/*@ <display>
Give below a formula G which is identical to F except that it has a separate
pair of parentheses ( ) around *every* logical connective and around *every*
quantifier:

  (¬...) (...∧...) (...∨...) (...⇒...) (...⇔...) (∀...) (∃...)

Thus the number of parenthesis pairs ( ) to be added equals the total number of
connectives and quantifiers in F.
</display> @*/

//@ <private>
pred withPar1(x:D) ⇔
//@ <public>
//@ <data id="task1help">
// Add here 3 pairs of parentheses ( )
//@ </data>
//@ <input id="task1input">
¬ p(x) ∧ q(x) ⇒ r(x)
//@ </input>
//@ <private>
;

theorem correctPar1(x:D) ⇔ withoutPar1(x) ⇔ withPar1(x);

/*@ <display>
</display>@*/
/*@ 
<button id="task1" label="Check Task 1" action="correctPar1">
<argument value="-opt-si"> <argument option="silent">
</button>
@*/

//@ <private>
/*@ <display>

TASK 2 DESCRIPTION: 
-----------------------------
Below you see a formula F without parentheses:
</display> @*/

pred withoutPar2(x:D) ⇔ 
//@ <public>
//@ <data id="task2data">
  ∃y:D. x + 1 = y
//@ </data>
//@ <private>
;

/*@ <display>
Give a definition of a formula G as described in the TASK 1 DESCRIPTION. However
*also* add in formula G a pair of parentheses ( ) around every application of an
infix function/predicate symbol:

   (...+...) (...=...) ...
</display>@*/

pred withPar2(x:D) ⇔
//@ <public>
//@ <data id="task2help">
// add here 3 pairs of parentheses ( )
//@ </data>
//@ <input id="task2input">
∃y:D. x + 1 = y
//@ </input>
//@ <private>
; 

theorem correctPar2(x:D) ⇔ withoutPar2(x) ⇔ withPar2(x);

/*@ 
<button id="task2" label="Check Task 2" action="correctPar2">
<argument value="-opt-si"> <argument option="silent">
</button>
@*/

/*@ <display>

TASK 3 DESCRIPTION: 
-----------------------------
Below you see the definition of a predicate by a formula F. Remove from the
parameter list all those variables x:D,... that are *not* free in F.
</display> @*/

//@ <public>
// remove here as many variables as possible
pred varFormula3(/*@<input id="task3input" cols="20">@*/x:D, y:D, z:D/*@</input>@*/) ⇔ 
//@ <data id="task3data">
  x < z ⇒ ∃y:D. y > 0 ∧ x+y = z
//@ </data>
; 
//@ <private>
/*@<display>
Your answer is correct, if removing any more variables (after pressing the
"Check" button) would give an error message.
</display>@*/

/*@ 
<button id="task3" label="Check Task 3" action="varFormula3">
<argument value="-opt-si"> <argument option="silent">
</button>
@*/

/*@<display>

TASK 4 DESCRIPTION: 
-----------------------------
Below you see the description of an informal statement.
</display>@*/
/*@<display id="task4data">

    x is greater than 0 and there is no such number
    (i.e., no number greater than 0) that is smaller than x
    (this means that x is the smallest number greater than 0.)
    
</display>@*/
/*@<display>
Give a definition of a predicate

   pred formula4(x:D,y:D,z:D) ⇔ F ;

with a formula F that expresses this statement in the *most literal* way (i.e.,
it should be a straight-forward translation from natural language to logic
operators).

Furthermore remove from "formula4(x:D,y:D,z:D)" all those variables that do
*not* occur freely in F.

Your answer is *very likely* correct if your definition (after pressing the
"Check" button does not give an error message and not the message "theorem is
not true".
</display>@*/
//@ <public>
// give here your formula F.
pred formula4(/*@<input id="task4input1" cols="20">@*/x:D, y:D, z:D/*@</input>@*/) ⇔ // remove variables
/*@<input id="task4input2" cols="40" rows="3">@*/
x > 0 ∧ ~∃y:D. y > 0 ∧ y < x
/*@</input>@*/  // replace "⊤"
; 
//@ <private>
theorem correctFormula4(x:D,y:D, z:D) ⇔ // remove variables
//@ <public>


// correspondingly remove variables from application of formula here
/*@<input id="task4input3">@*/formula4(x,y,z)/*@</input>@*/ 
//@ <private>  
  ⇔
  x = 1
; 
/*@ <button id="task4" label="Check Task 4" action="correctFormula4">
    <argument value="-opt-si"> <argument option="silent">
    </button>
  @*/


// =============================================================
// END OF FILE
// =============================================================