Computational Formal Semantics: Propositional and First-Order Logic

Plan for the May 7 (11 am-12 pm) meeting: we’ll go through the implementation of propositional and first-order logic in the “Computational Semantics” textbook. This material is discussed in chapters 4, 5 and 6 of the textbook interspersed with various other topics. Jan van Eijck and Christina Unger (the authors of the textbook) have graciously allowed us to link to re-organized parts of their code on this site. For the complete original code, see here.

From now on, the Haskell scripts will be organized in groups based on the main topic they address.

The first topic is propositional logic. We have a module defining the syntax of propositional logic PropLsyn.hs, a module defining the corresponding semantics of propositional logic PropLsem.hs, and the GHCI script PropLghci.hs we will use in the meeting to introduce and interact with these modules. You should place all these files in the same folder.

The second topic is first-order logic (FOL). Just as for prop. logic, we have a module defining the syntax of FOL PredLsyn.hs, a module defining the corresponding semantics of FOL PredLsem.hs, a distinct module defining a particular FOL model Model.hs and finally, the GHCI script PredLghci.hs we will use in the meeting to introduce and interact with all these modules. Again, you should place all these files in the same folder.

Note that because of the additional complexity of FOL, we chose to separate the recursive definition of truth and satisfaction for FOL (PredLsem.hs) and the definition of a particular model (Model.hs) relative to which we can evaluate FOL formulas.