Refine
Has Fulltext
- yes (2)
Document Type
- Bachelor Thesis (1)
- Doctoral Thesis (1)
Language
- English (2)
Is part of the Bibliography
- yes (2)
Keywords
- Argumentation (1)
- Beweis (1)
- Beweisassistent (1)
- Beweisumgebung (1)
- Coq (1)
- Curry (1)
- Formalismus (1)
- Formalitätsgrad (1)
- Gleichheit (1)
- Konnektionskalkül (1)
- Logik (1)
- Mathematikdidaktik (1)
- Mathematikphilosophie (1)
- Omega (1)
- TPTP (1)
- Taktik (1)
- argumentation (1)
- arithmethische Prozeduren (1)
- arithmetic procedures (1)
- automatic theorem prover (1)
- automatisierter Theorembeweiser (1)
- connection calculus (1)
- degree of formality (1)
- equality (1)
- formalism (1)
- leanCoP (1)
- logic (1)
- mathematics education (1)
- omega (1)
- philosophy of mathematics (1)
- proof (1)
- proof assistant (1)
- proof environment (1)
- tactic (1)
- tptp (1)
Institute
In this thesis we introduce the concept of the degree of formality. It is directed against a dualistic point of view, which only distinguishes between formal and informal proofs. This dualistic attitude does not respect the differences between the argumentations classified as informal and it is unproductive because the individual potential of the respective argumentation styles cannot be appreciated and remains untapped.
This thesis has two parts. In the first of them we analyse the concept of the degree of formality (including a discussion about the respective benefits for each degree) while in the second we demonstrate its usefulness in three case studies. In the first case study we will repair Haskell B. Curry's view of mathematics, which incidentally is of great importance in the first part of this thesis, in light of the different degrees of formality. In the second case study we delineate how awareness of the different degrees of formality can be used to help students to learn how to prove. Third, we will show how the advantages of proofs of different degrees of formality can be combined by the development of so called tactics having a medium degree of formality. Together the three case studies show that the degrees of formality provide a convincing solution to the problem of untapped potential.
In this bachelor’s thesis I implement the automatic theorem prover nanoCoP-Ω. This system is the result of porting arithmetic and equality handling procedures first introduced in the automatic theorem prover with arithmetic leanCoP-Ω into the similar system nanoCoP 2.0. To understand these procedures, I first introduce the mathematical background to both automatic theorem proving and arithmetic expressions. I present the predecessor projects leanCoP, nanoCoP and leanCoP-Ω, out of which nanCoP-Ω was developed. This is followed by an extensive description of the concepts the non-clausal connection calculus needed to be extended by, to allow for proving arithmetic expressions and equalities, as well as of their implementation into nanoCoP-Ω. An extensive comparison between both the runtimes and the number of solved problems of the systems nanoCoP-Ω and leanCoP-Ω was made. I come to the conclusion, that nanoCoP-Ω is considerably faster than leanCoP-Ω for small problems, though less well suited for larger problems. Additionally, I was able to construct a non-theorem that nanoCoP-Ω generates a false proof for. I discuss how this pressing issue could be resolved, as well as some possible optimizations and expansions of the system.