diff --git a/MyCommentedIsabelle.thy b/MyCommentedIsabelle.thy index 10382d69..83c9e224 100644 --- a/MyCommentedIsabelle.thy +++ b/MyCommentedIsabelle.thy @@ -456,7 +456,7 @@ fn name => (Thy_Output.antiquotation name (Scan.lift (Parse.position Args.cartou \ subsection\ Markup \ -text{* Markup Operations, and reporting. *} +text{* Markup Operations, and reporting. Diag in Isa_DOF Foundations Paper. *} ML{* (* Markup.enclose; *) diff --git a/examples/math_exam/BAC2017/BAC2017.thy b/examples/math_exam/BAC2017/BAC2017.thy index e1ce146d..ac7e96fc 100644 --- a/examples/math_exam/BAC2017/BAC2017.thy +++ b/examples/math_exam/BAC2017/BAC2017.thy @@ -1,5 +1,5 @@ theory BAC2017 - imports "../../../ontologies/mathex_onto" + imports "../../ontologies/mathex_onto" Deriv Transcendental begin diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy index f9e92de2..92b82e41 100644 --- a/examples/math_exam/MathExam/MathExam.thy +++ b/examples/math_exam/MathExam/MathExam.thy @@ -8,7 +8,7 @@ open_monitor*[exam::MathExam] section*[idir::Author, affiliation="''CentraleSupelec''", email="''idir.aitsadoune@centralesupelec.fr''"] -{*Idir AIT SADOUNE*} + {*Idir AIT SADOUNE*} subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1''", date="''02-05-2018''", timeAllowed="90::int"] diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index 786e28a2..c8625426 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -1,7 +1,27 @@ theory mathex_onto imports "../Isa_DOF" begin + +text{* In our scenario, content has four different types of addressees: +\<^item> the @{emph \setter\}, i.e. the author of the exam, +\<^item> the @{emph \student\}, i.e. the addressee of the exam, +\<^item> the @{emph \checker\}, i.e. a person that checks the exam for +\<^item> the @{emph \external_examiner\}, i.e. a person that checks the exam for + feasibility and non-ambiguity. +Note that the latter quality assurance mechanism is used in many universities, +where for organizational reasons the execution of an exam takes place in facilities +where the author of the exam is not expected to be physically present. +*} + + +datatype ContentClass = + setter -- \the 'author' of the exam\ + | checker -- \the 'proof-reader' of the exam\ + | external_examiner -- \the 'proof-reader' of the exam\ + | student -- \the victim ;-) ... \ + + doc_class Author = affiliation :: "string" email :: "string" @@ -12,17 +32,6 @@ datatype Subject = datatype Level = oneStar | twoStars | threeStars -text{* In our scenario, content has three different types of addressees: -\<^item> the @{emph \examiner\}, i.e. the author of the exam, -\<^item> the @{emph \student\}, i.e. the addressee of the exam, -\<^item> the @{emph \validator\}, i.e. a person that checks the exam for - feasibility and non-ambiguity. - -Note that the latter quality assurance mechanism is used in many universities, -where for organizational reasons the execution of an exam takes place in facilities -where the author of the exam is not expected to be physically present. - *} - datatype Grade = A1 | A2 | A3 @@ -33,11 +42,6 @@ doc_class Header = date :: string timeAllowed :: int -- minutes -datatype ContentClass = - examiner -- \the 'author' of the exam\ - | validator -- \the 'proof-reader' of the exam\ - | student -- \the victim ;-) ... \ - doc_class Exam_item = concerns :: "ContentClass set" @@ -58,18 +62,18 @@ doc_class Task = Exam_item + level :: Level type :: Question_Type subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list" - concerns :: "ContentClass set" <= "{examiner,validator,student}" + concerns :: "ContentClass set" <= "{setter,student,checker,external_examiner}" mark :: int doc_class Exercise = Exam_item + content :: "(Task) list" - concerns :: "ContentClass set" <= "{examiner,validator,student}" + concerns :: "ContentClass set" <= "{setter,student,checker,external_examiner}" text{* In many institutions, it makes sense to have a rigorous process of validation for exam subjects : is the initial question correct ? Is a proof in the sense of the -question possible ? We model the possibility that the @{term examiner} validates a +question possible ? We model the possibility that the @{term setter} validates a question by a sample proof validated by Isabelle. In our scenario this sample proofs are completely @{emph \intern\}, i.e. not exposed to the students but just additional material for the internal review process of the exam.*} @@ -81,11 +85,11 @@ doc_class Validation = doc_class Solution = Exam_item + content :: "Exercise list" valids :: "Validation list" - concerns :: "ContentClass set" <= "{examiner,validator}" + concerns :: "ContentClass set" <= "{setter,checker,external_examiner}" doc_class MathExam= content :: "(Header + Author + Exercise) list" global_grade :: Grade where "\Author\\<^sup>+ ~~ Header ~~ \Exercise ~~ Solution\\<^sup>+ " - + end \ No newline at end of file