|
|
|
|
| Bachelorprojekt - Softwareteknologi | Project No. 0178: Prover Programming |
| Aktuelle | Tidligere |
Mathematical logic is used for the formalization of systems and results in computer science and mathematics. Provers are the main formalization technology and are often implemented in declarative programming languages, for example the functional programming languages F# or SML, but logic programming languages like ISO Prolog or Visual Prolog can be used too. Furthermore, proof assistants like Isabelle can formalize algorithms and logical inference systems, both abstractly and concretely.
The purpose of the project is to develop and evaluate a prototype of a prover for first-order logic, but higher-order logic or type theory can also be considered, and the prover can be automatic or interactive.
| Prerequisites: | 02156 Logical Systems and Logic Programming |
Restrictions: Max 2 projects
Supervisor(s) Jørgen Villadsen
| Sidst opdateret: Nov 24, 2021 af Carsten Witt |