2018-04-17 14:43:08 +00:00
|
|
|
theory MathExam
|
|
|
|
imports "../../ontologies/mathex_onto"
|
|
|
|
begin
|
|
|
|
|
|
|
|
open_monitor*[exam::MathExam]
|
|
|
|
|
|
|
|
text*[idir::Author, affiliation="CentraleSupelec"]{*Idir AIT SADOUNE*}
|
|
|
|
|
2018-04-18 07:36:21 +00:00
|
|
|
text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="Exam number 1"]
|
2018-04-17 14:43:08 +00:00
|
|
|
{* Please follow directions carefully ans show all your work.*}
|
|
|
|
|
2018-04-18 07:36:21 +00:00
|
|
|
|
|
|
|
section*[exo1 :: Exercise, content="[q1,q2,q3]"]{* Exercise 1.*}
|
|
|
|
text*[q1::Question, level="twoStars", mark="5"]
|
2018-04-17 14:43:08 +00:00
|
|
|
{*
|
|
|
|
Give an example of each of the following :
|
|
|
|
a - a rational number which is not integer.
|
|
|
|
b - a real number which is not rational.
|
|
|
|
*}
|
|
|
|
|
2018-04-18 07:36:21 +00:00
|
|
|
text*[q2::Question, level="oneStar", mark="5"]
|
2018-04-17 14:43:08 +00:00
|
|
|
{*
|
|
|
|
Write in interval notation : @{term ''-3 < x < 5''}
|
|
|
|
*}
|
|
|
|
|
2018-04-18 07:36:21 +00:00
|
|
|
text*[q3::Question, level="oneStar", mark="5"]
|
2018-04-17 14:43:08 +00:00
|
|
|
{*
|
|
|
|
True or false : @{term ''0/8 = 0''}
|
|
|
|
*}
|
|
|
|
|
2018-04-18 07:36:21 +00:00
|
|
|
close_monitor*[exam]
|
|
|
|
|
|
|
|
end
|
|
|
|
|
2018-04-17 14:43:08 +00:00
|
|
|
(*
|
|
|
|
|
|
|
|
section{* Example*}
|
|
|
|
|
|
|
|
term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ] "
|
|
|
|
|
|
|
|
text{*
|
|
|
|
@{term "[ @{thm ''refl''}] @ [ @{thm ''sym''}, @{thm ''trans''} ]"}} are the theorems
|
|
|
|
of the equational logic fragment of HOL.
|
|
|
|
*}
|
2018-04-18 07:36:21 +00:00
|
|
|
*)
|