Library for Verifying the Solutions of Predicate Calculus
Name
Siiri Saar
Abstract
The goal of this bachelor thesis is to implement a library for verifying the solutions to the provided sentences of the predicate calculus. The library is intended to be used in automatizing the examination of students' answers in the predicate calculus courses in Tartu Ülikool. At present, the lab instructors check the answers manually.
The implemented library contains methods that verify the user input from two aspects – the input is syntactically correct and it expresses the given sentence. Input is deemed syntactically correct if it contains the constant, functional and predicate symbols that are permitted with the arithmetic signature of σ = <0, 1; +, *; =>, a balanced amount of brackets and the helper predicates defined beforehand. For helper predicates, the program also checks the correct usage of free variables, defined as follows – all free variables used in the predicate are provided as arguments to the predicate and all the predicate's arguments are free variables in the predicate.
To check if the user provided formula is equivalent to a correct formula, the program deploys two methods. First, it applies a method called the truth tree, which consists in analysing the logical structure of the equivalence formula, made up of the user input and the correct answer. The second method consists of evaluating the two formulas with a limited set of natural numbers and checking if the formulas' truth values coincide.
Verifying the equivalence of two formulas is a problem that is known to be algorithmically unsolvable. The two selected methods complement each other – the truth tree method allows determining the equivalence of two formulas, while the brute-force evaluation allows determining their non-equivalence.
The implemented library contains methods that verify the user input from two aspects – the input is syntactically correct and it expresses the given sentence. Input is deemed syntactically correct if it contains the constant, functional and predicate symbols that are permitted with the arithmetic signature of σ = <0, 1; +, *; =>, a balanced amount of brackets and the helper predicates defined beforehand. For helper predicates, the program also checks the correct usage of free variables, defined as follows – all free variables used in the predicate are provided as arguments to the predicate and all the predicate's arguments are free variables in the predicate.
To check if the user provided formula is equivalent to a correct formula, the program deploys two methods. First, it applies a method called the truth tree, which consists in analysing the logical structure of the equivalence formula, made up of the user input and the correct answer. The second method consists of evaluating the two formulas with a limited set of natural numbers and checking if the formulas' truth values coincide.
Verifying the equivalence of two formulas is a problem that is known to be algorithmically unsolvable. The two selected methods complement each other – the truth tree method allows determining the equivalence of two formulas, while the brute-force evaluation allows determining their non-equivalence.
Graduation Thesis language
Estonian
Graduation Thesis type
Bachelor - Computer Science
Supervisor(s)
Reimo Palm
Defence year
2017