You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Stefan Pranger 9f78aab258 updated solution for z3 0003 8 months ago
1_smt_and_z3 updated solution for z3 0003 8 months ago
2_propositional_logic removed duplicate counter 10 months ago
3_sat_solvers_dpll fixed typo in chapter three 0002 sol 8 months ago
4_natural_deduction_propositional_logic added solutions for ass sheet 5 10 months ago
4_tseitin removed duplicate counter 10 months ago
5_predicate_logic fixed phrasing in pred logic 1001 8 months ago
6_natural_deduction_predicate_logic added solutions for ass sheet 7 10 months ago
7_smt added solutions for ass sheet 7 10 months ago
8_bdds fixed solution in bdd 0007 8 months ago
9_equivalence_checking fixed solution cec 0009 8 months ago
10_symbolic_encoding added chapter ten 9 months ago
11_temporal_logic fixed phrasing and solution TL 0006 8 months ago
figures added chapter eleven temporal logic 9 months ago
util compile missing chapters 9 months ago
.drone.yml refined drone conditions 9 months ago
Makefile added framework files 12 months ago added link to SS22 version 1 year ago
compile added framework files 12 months ago
main.tex added chapter eleven temporal logic 9 months ago
no_solution.tex added framework files 12 months ago
solution_boilerplate.tex added framework files 12 months ago

Questionnaire for Logic and Computability

If you're taking the exam on the 9th of March, you can find the SS22 version of the questionnaire here.

! Version SS23 !

How to use this questionnaire

This questionnaire should help you study for the final lecture exam for Logic and Computability. It comes in three different fashions:

  • The basic questionnaire with the list of possible questions for the exam,
  • the same questionnaire with additional space to fill in your solutions with a pen and
  • the questions with all currently available solutions.

The questionnaire comes with three different tags for each question:

  • [Lecture]: Questions that will be solved during the lecture on Friday. Solutions will be provided by us after the lecture.
  • [Practical]: Questions part of the assignments of the practicals. Solutions will be provided by us after the corresponding practicals.
  • [Self-Assessement]: Questions for self-assessment.

We allow and encourage you to discuss and post solutions for the [Self-Assessement]-questions. We will carry together all of the solutions such that you will have a rich set of questions and solutions for your studies at the end of the semester.

You can find the current version of the questionnaire in the Releases tab of this repository.


You do not need to build the questionnaire locally. All versions will be released here.

In case you want to contribute or adapt the questionnaire to you liking you first have to clone this repository:

git clone

Install the dependencies:

sudo apt-get install latexmk texlive-luatex texlive-latex-recommended

This is currently not exhaustive, i.e. there might be other packages needed.

Feel free to open a PR with dependencies for other distros.

The whole questionnaire can now be built using the shipped shell script:


We support different <version>s: 'blank', solution, spacing and all. Compiling with the -b option will burst all sections into individual files. This respects the version you may define.

Run ./compile -h to print the help message:

A shell wrapper for this questionnaire using latexmk.
Currently this wrapper supports compiling of the whole script and a burst mode,
as well as three different <version>s: 'blank', solution, spacing and all which will compile all three in one run.

Usage: ./compile <flags> <version>
 -b     Compile in burst mode, i.e. each chapter into a individual file.
 -d     Print LuaLaTeX output to terminal.
 -h     Print this help message and exit.


If you want to contribute your solutions for questions tagged with [Self-Assessement] you are very welcome to open a pull request or send us your solution files via email.

A handy way to split up LaTeX source code is to use the \input{...} statement.

For a simple way to compile your solutions while writing them up, we have provided a separate LaTeX main file called simple.tex which uses the same packages as the main file for the questionnaire. In order to only compile your solution put them into a separate my_solution.tex file and compile them with lualatex simple.

Note that every solution needs to have its own solution file. If you want to contribute using a PR please stick to the naming convention, i.e. suffix a _sol to the question you're answering in that file. E.g.:

X_chapter/theory_questions/1_1_topic_self will have its solution in X_chapter/theory_questions/1_1_topic_self_sol.

           {question_file_with_solutions} <-- your file name goes here
         {solution} <-- your file name goes here

If you send us your solutions we will take care of that. Please be sure to name the input files according to the question you have answered.