This 2006 paper (written in German, "Algorithmische Aspekte der klassischen und philosophischen Logik") traces the procedure of automatically treating a given sentence of Natural Language.

## Abstract

This paper presents various aspects of the use of algorithms in propositional and first order logic. The history of logic automata and of the notion ‘algorithm’ itself is outlined in the first chapter—followed by the declaration of the pseudo code notation used for presenting different implementations in the text. The next chapters follow the process of treating a given natural language proposition with automated procedures. Chapter 2 discusses a symbolization strategy suggested by Godehard Link in Collegium Logicum—Logische Grundlagen der Philosophie [Link 2003] (enclosed as appendix A), especially with respect to the so called “donkey sentences” and their treatment in Discourse Representation Theory. The subject of chapter 3 is the conversion of first order formulas into Prenex Normal Form. Here an algorithm for PNF conversion on the basis of tree structures is established and a graphical implementation in the object oriented programming language Java is discussed. Chapter 4 gives an overview over applied automated proof

strategies, especially with regard to Herbrand’s Theorem. The paper concludes with the discussion of an algorithm as decision procedure for propositional formulas, the Quine Analysis, as described in [Link 2003].

## Keywords

Automata, Algorithms, Formalization of Natural Language, Prenex Normal Form Conversion (implemented), Tree Representation of Formulae, Herbrand Expansion, Tableaux with Unification, Skolemization, Quine Analysis (implemented)

## Supplement

The paper was originally intended to be supplemented with a CD-Rom containing graphical implementations of PNF conversion (chpt. 3) and Quine Analysis (chpt. 5) as a platform-independent Java program that utilizes tree structures for analyzing and manipulating formulas. The program can now be found online as Logics Pack Console. Selected code blocks are shown in print in appendix D.