Propositional Logic Prover I: Parser

Learn techniques to build a parser for propositional logic.

Introduction

The purpose of creating a propositional logic parser is to develop a program or tool that can analyze and interpret propositions written in propositional logic notation. This parser will be able to parse input strings, validate their syntax and output an abstract syntax tree (AST). In later projects, the generated AST will be used to evaluate the truth values of logical expressions and so much more. It can also serve as a fundamental component for more advanced logical reasoning systems.

You can find the full code in my github repo.

Prerequisites

Here are the concepts you need to know to understand the text in this project:

The tools needed for this project:

Check your knowledge

Can you explain what a PEG is?

In parsing, a PEG (Parsing Expression Grammar) is a type of formal grammar used to describe the syntax of a language. PEGs are similar to context-free grammars, but they have some key differences that make them particularly useful for parsing tasks. For example, a PEG grammar is deterministic, so each input can only be parsed in one way.

Can you create a propositional logic formula for the following sentence: 'If it rains, then the ground is wet'?

We can first replace 'it rains' by $A$ and 'the ground is wet' by $B$, then we can write the formula as $A\rightarrow B$.

Overview

In this project, we will design and implement a propositional logic parser that can handle various types of propositional logic expressions, such as negations, conjunctions, disjunctions, implications, equivalences, and their combinations. The parser should employ efficient algorithms to parse these expressions accurately. We will explore two practical applications of the parser, such as generating visual representations from input strings representing well-formed formulas (WFFs) and implementing a method to convert these objects back to strings.

Objectives

The main objectives of this project include:

  1. Defining a formal language for propositional logic.
  2. Creating a parser for that language.
  3. Converting an input wff string into a WFF object.
  4. Visualizing the WFF object as an AST image.
  5. Designing and implementing a method for transforming a WFF object back into a string.
We start with a WFF string and after parsing we obtain a tree data structure representing the WFF.

Figure 1. Visual example of what we want to achieve from steps 1 to 3. We start with a WFF string and after parsing we obtain a tree data structure representing the WFF.

By achieving these objectives, we aim to create a reliable propositional logic parser that can simplify and streamline the process of analyzing and evaluating propositional logic expressions.