The Method of Variable Splitting
@PhdThesis{Antonsen08,
author = {Roger Antonsen},
title = {The {M}ethod of {V}ariable {S}plitting},
school = {University of Oslo},
year = 2008,
key = {Automated Reasoning, Logic, Proof Theory, Connection Method, Tableau Calculus},
address = {Department of Informatics},
month = {June}
} Abstract
This is a thesis in the intersection of automated reasoning and proof theory. It is in the field of automated reasoning because it is a detailed analysis of certain search space redundancies that, in the end, may lead to more efficient theorem provers. It is in the field of proof theory because formal proofs and properties of such are analyzed in great detail. The thesis is foundational in nature and investigates the fundamentals and the metatheory of a method called variable splitting.
Phd Thesis
- PhD Thesis: The Method of Variable Splitting (PDF)
- Announcement of PhD defence, 2008 (in Norwegian)
- Short Description (PDF)
- Announcement of trial lecture, 2008 (in Norwegian)
In his thesis, done at the Department of Informatics at the University of Oslo, Roger Antonsen formed the theoretical basis for a method that could potentially lead to an improvement of automatic reasoning and theorem proving.
The study of how to get machines to think or reason has blossomed along with the development of computers and information technology. This field, called automatic reasoning, has many applications. Using symbolic tools, one can represent and process knowledge and in this way create computer programs that, for example, assist people in complex decision making or searching for formal proofs for assertions and theorems within mathematics. It is about getting computers to be able to calculate conclusions from premises or to derive new knowledge from already given data. This is usually very complex and requires precise and effective search mechanisms.
Antonsen's thesis is in intersection of mathematical logic, automatic reasoning, and proof theory, and borders on areas like artificial intelligence, decision theory, knowledge representation, and complexity theory. It defines a mathematical tool that can be used to identify and remove specific redundancies in logical calculi used for automated reasoning. The method, which is based on a detailed analysis of the dependencies between universal expressions – "for all" formulas – and branching expressions – "or" formulas –, forms the basis of improving the efficiency of automated search. In his thesis, Antonsen treats a number of different logical systems and looks at how the method can be applied to these. Through new mathematical results, it is among other things demonstrated how the method can give rise to exponential improvements in automated search.
