Skip to content

Glossary

Jump to bottom
Kevin Weirauch edited this page Jul 11, 2019 · 28 revisions

Preface

In the following you can find a listing of some technichal and project related terms. This list does not claim to be complete, so any recommendation for extending it is welcome.

The terms themselves will mostly be in english with their german equivalent being mentioned at least once. For certain terms mostly the german term will be used and the english equivalent will be mentioned at least once. This is because some terms (mostly the GUI-related ones) will be displayed to the user in german. If none equivalent is mentioned then the term can be used equivalently in both languages.

The glossary will be in alphabetical order.

Glossary

Arity

The arity (Arität / Stelligkeit) of a function f in Logic and by extension in the Diproche system is a natural number stating the amount of arguments f takes as input. If the inputs can have different sorts than the arity additionally consists of a tuple (sort1, sort2, ..., sortn) that states which argument has to be of which sort.

Aussagenlogisches Beweisen

Aussagenlogisches Beweisen (Proofs in Propositional Logic) is a Spielwiese in the Diproche system.

Code (Attribute)

Code is an attribute of an Issue. It stands for the kind of issue that occured. The different possible kinds of issues currently are:

  • BRACKET_UNDERCLOSING - When at least one open bracket is not closed
  • BRACKET_OVERCLOSING - When at least one bracket that is closed is not opened
  • EMPTY_BRACKET - When a bracket contains nothing or any amount of Whitespaces
  • INVALID_WORD - When a word is not allowed to be used
  • MISSING_CONNECTOR - When a boolean connective is missing
  • MISSING_STATEMENT_INSIDE - Please edit
  • MISSING_STATEMENT_AFTER_NEGATION - When there is a negation with no formula afterwards
  • UNVERIFIED_LINE - When a line of a proof can't be verified

Constant

A constant (Konstante) in Logic and by extension in the Diproche system is a function with arity 0.

Diproche

Diproche stands for "Didactical Proof Checking". It has the goal to check proofs for mathematical propositions that are formulated in natural language in a controlled way.

Example

An example (Beispiel) in the Diproche system is a combination of an exercise and an explanation on how to solve this exercise. It should teach the user to

  • formulate his proofs in a correct way;
  • formulate his proofs in a way the system can read and process it.

Exercise

An exercise (Übungsaufgabe) is a (well-formed) task in the Diproche system. It can also state limitations regarding the proof technique or give hints a priori.

Function

A function (Funktion) in Logic and by extension in the Diproche system is a mapping that takes some amount of elements of a domain and maps them to a single element of a codomain. If the function does not need any elements it is also called a constant.

Goal

A goal (Ziel) in the [Diproche][https://github.com/diproche/webinterface/wiki/Glossary#Diproche) system is a well-formed mathematical sentence that can be proven. In this case "well-formed" refers to a well-formed formula of first order logic.

Impressum

The impressum is a component of the webinterface. There is no difference between the Impressum in the Diproche system and a common Impressum.

Issue

An issue (Problem) in the Diproche system is an interface with which a mistake of any kind made by the user can be saved in a systematical way. It can be found in the file Issue.ts. It has one optional and three necessary attributes:

Message (Attribute)

message (Nachricht) is one of the attributes of an issue. It is a string which tells the user what his mistake was and where he can find it. It should be as constructive as possible.

Position (Attribute)

position is one of the attributes of an issue. It is of type Position.

Position (Interface)

Position is an interface in the Diproche system consisting of two arguments:

  • fromIndex: number - the index at which a mistake starts
  • toIndex: number - the index at which a mistake ends

Predicate

A predicate (Prädikat) in Logic and by extension in the Diproche system is a function having as codomain the truthvalues 0 (false) and 1 (true).

Severity (Attribute)

The severity (Schwere) of an issue is a string stating how severe the issue is. It can take one of the following values:

  • ERROR
  • FATALERROR
  • HINT
  • WARNING

Spielwiese

A Spielwiese (playground) in the Diproche system is a collection of tasks that all belong to the same topic. It also has a name.

Task

A task (Aufgabe) in the Diproche system consists of a goal that should be proved. Furthermore it is called well-formed if it also states every axiom that can be used.

An example for a task would be: Prove the Pythagorean Theorem.

An example of a well-formed task with the same goal would be: Let ABC be a right triangle with sides a, b, c. Prove the Pythagorean Theorem.

Term

A term is in Logic and by extension in the Diproche system is recursively defined by:

  • Every variable is a term
  • If t1, t2, ..., tn are terms, then so is f(t1, t2, ..., t_n) if f has arity n.

Termvaluation

A termvaluation of a term in Logic and therefore in the Diproche system is a function that associates a term with a concrete value. For example: Given the fact, that the predicate female(anna) returns true, then a termvaluation of female(x) would be female(anna).

Vocabulary Checker

The vocabulary checker (Vokabularprüfer) is a component of the Diproche system. It detects, if the user uses a word he is not allowed to used. The checker consists of everything in the file detectWrongSyntax.ts. All allowed words can be found in the file allowedVocab.json.

Webinterface

The webinterface in the Diproche system refers to the interface of the webapplication. It aims to be

  • helpful
  • intuitive
  • user friendly

Clone this wiki locally