Computational Logic Lab 2011 (EMCL-FUB)

EMCL-FUB Computational Logic Lab 2011 (Camilo Thorne)
In the labs, projects and assignments of the course we'll use the Objective Caml (OCaml) programming language, used in the main textbook of the course, Harrison's "Handbook of Practical Logic and Automated Reasoning ", whose code can be downloaded here. Other known tools for FOL and propositional logic are: Minisat (state-of-the-art propositional SAT solver). SPASS (state-of-the-art resolution-based FOL reasoner). Prover9 and Mace (FOL reasoner and FOL model builder, resp.). Bliksem (resolution-based FOL reasoner). Lab 25.02.2011 - OCaml. In this lab we introduce the OCaml programming language and the environment. Caml (Categorical Abstract Machine Language) is a high-level, functional, strongly- and statically-typed interpreted programming language. OCaml is its object-oriented extension, supporting also imperative programs on top of its purely functional fragment. Lab 04.03.2011 - Propositional Logic (I). The exercise sheet is here. Solutions to some exercises can be found here. Lab 11.03.2011 - Propositional Logic (II). The exercise sheet is here. Lab 18.03.2011 - Propositional Logic (III). The exercise sheet is here. Lab 25.03.2011 - Propositional Logic (IV) The exercise sheet is here. Lab 01.04.2011 - Propositional Logic (V). The exercise sheet is here.

EMCL-FUB Computational Logic Lab 2011 (Camilo Thorne)

In the labs, projects and assignments of the course we'll use the Objective Caml (OCaml) programming language, used in the main textbook of the course, Harrison's "Handbook of Practical Logic and Automated Reasoning ", whose code can be downloaded here. Other known tools for FOL and propositional logic are:

Minisat (state-of-the-art propositional SAT solver).
SPASS (state-of-the-art resolution-based FOL reasoner).
Prover9 and Mace (FOL reasoner and FOL model builder, resp.).
Bliksem (resolution-based FOL reasoner).

Lab 25.02.2011 - OCaml. In this lab we introduce the OCaml programming language and the environment. Caml (Categorical Abstract Machine Language) is a high-level, functional, strongly- and statically-typed interpreted programming language. OCaml is its object-oriented extension, supporting also imperative programs on top of its purely functional fragment.
Lab 04.03.2011 - Propositional Logic (I). The exercise sheet is here. Solutions to some exercises can be found here.
Lab 11.03.2011 - Propositional Logic (II). The exercise sheet is here.
Lab 18.03.2011 - Propositional Logic (III). The exercise sheet is here.
Lab 25.03.2011 - Propositional Logic (IV) The exercise sheet is here.
Lab 01.04.2011 - Propositional Logic (V). The exercise sheet is here.