Supplementary Material for "Oblig 2"

Logic for Computer Science (UiO) - Autumn 2017


Shell Script and Prolog Program Frame for O2.2/O2.3

These program frames can (but don't have to) be used in order to implement the propositional (and first-order) theorem prover in Prolog.

Test Formulae for O2.2/O2.3

These test formulae can (but don't have to) be used in order to test the propositional (and first-order) theorem prover. All formulae should be valid/theorems (for classical logic). Changing (the right) predicate symbols or logical operators will (usually) result in formulae that are invalid (for testing correctness).

















Jens Otten (University of Oslo) 14.11.2017