Documentation

Installing Logic1

If you already have an Anaconda installation then goto Step 3.
Install Miniconda

"Conda is an open-source package management system and environment management system that runs on Windows, macOS, and Linux. Conda quickly installs, runs, and updates packages and their dependencies. Conda easily creates, saves, loads, and switches between environments on your local computer. It was created for Python programs but it can package and distribute software for any language."

This means: You can install and temporarily use one or several alternative Python installations and their packages without interfering with your existing system in any way. Everything is kept together in one directory (which can be easily deleted when not wanted anymore).
Get the latest Miniconda installer for your OS.
Follow the installation instructions for your OS here.
Caveat: By default, the Conda installers modify your shell profiles on Unix systems (I do not know about Windows).
With the bash installer, this can be avoided by not adimitting "conda init" when asked interactively. Note that "conda init" can be called explicitly anytime. With the graphical installer, there is a "Customize" button at the bottom of the "Installation Type" page, which allows to remove a corresponding checkmark.
Here is the code that got inserted into .bash_profile for me (on Mac OS):
```
    # >>> conda initialize >>>
    # !! Contents within this block are managed by 'conda init' !!
    __conda_setup="$('/Users/sturm/miniconda3/bin/conda' 'shell.bash' 'hook' 2> /dev/null)"
    if [ $? -eq 0 ]; then
     eval "$__conda_setup"
    else
     if [ -f "/Users/sturm/miniconda3/etc/profile.d/conda.sh" ]; then
         . "/Users/sturm/miniconda3/etc/profile.d/conda.sh"
     else
         export PATH="/Users/sturm/miniconda3/bin:$PATH"
     fi
    fi
    unset __conda_setup
    # <<< conda initialize <<<
```
When the installation has finished, update conda:
```
    conda update -n base -c defaults conda
```
Create a new environment "qe":
```
    conda create --name qe
```
Activate your environment:
```
    conda activate qe
```
The active environment can be checked as follows:
```
    conda env list
```
The activation of the environment applies to the current shell. If you work only with qe, you might want to add "conda activate qe" to your profiles.
Conda installations:
Surprisingly little is needed; make sure that your active environment is "qe":
```
    conda install pip mypy pytest sympy jupyter
```
Pip installations (updated 2023-04-19):
Download logic1-0.1.1-py3-none-any.whl and make sure that your active environment is "qe":
```
    pip install logic1-0.1.1-py3-none-any.whl
```
This will also install Pyeda as a dependency.
Attention new version fixes bug:
Lorenz had found a bug in Logic1 0.1 originally posted here as logic1-0.1-py3-none-any.whl. The truth value F printed as T. To upgrade to the fixed version 0.1.1 above use:
```
    pip install --force-reinstall logic1-0.1.1-py3-none-any.whl
```

Exercises

2023-04-12:

Assignment:

Write a recursive simplifier for the ordered field of real numbers over the language of rings:

Simplify occurrences of T, F:

Eq(f, 0) & T becomes Eq(f, 0), Eq(f, 0) & F becomes F, etc.
Remove quantifiers when the variable does not occur:

Ex(x, Eq(y, 0)) becomes Eq(y, 0), etc.
Move negation inside using de Morgan's laws, apply involution, and finally encode in relations:

~ (Eq(a, 0) & Lt(b, 0) becomes Ne(a, 0) | Ge(b, 0), etc.
Evaluate:

Le(4, 5) becomes T, etc.
Make right hand sides of polynomial constraints zero:

Eq(f, g) becomes Eq(f - g, 0), etc.
Make left hand side polynomials primitive (gcd of integer coefficients = 1) with positive leading coefficients:

Lt(-8 * x + 6, 0) becomes Gt(4 * x + 3, 0), etc.
Smart-simplify constraints with equal left hand sides in conjunctions and disjunctions:

Lt(f, 0) | Eq(f, 0) becomes Le(f, 0), Lt(f, 0) & Eq(f, 0) becomes F, etc.
Sort argument subformulas of commutative logic operators:

SymPy should provide sorting of polynomials, also consider relations.

Use doctests, check code coverage, develop test data (share with others).

Tests:

There is not much simplification exepected in the following benchmarks. However, the CPU time should stay below 100 ms for each of the two examples. In the last exercise session we had observed unexpected timings in the range of seconds. It might be SymPy. We still have to understand this. Please check your implementations and report back.

Notice the magic command %timeit in the jupyter notebook files.

2023-04-26:

Download your preferred archive format. It will unpack as a directory named "qe":

qe.tgz, qe.zip

Here is the notebook from the exercise session on 2023-04-26:

zmodqe.ipynb

2023-05-10:

Assignment:

Implement QE for the class Sets.

Tests:

The following is the notebook that we had discussed originally:

map-coloring.ipynb

The following notebook (added 2023-05-31) covers the computations in Section 5.2 of the lecture notes:

map-coloring-lnqe.ipynb

2023-06-06:

Assignment:

Implement QE for Divisible ordered Abelian groups (Fourier–Motzkin Elimination)

Tests:

From the lecture notes:

Exercise at the end of 5.3 in the lecture notes
Use Case: Linear Programming (Section 7.5 of the lecture notes)

For examples from REMIS, look at the plain or formatted input files. Some discussion of the examples and results with other QE software can be found here:

The Collins–Johnson Problem in the form "lwcoj"
MTP-2 (all x are existentially quantified, all a, b, c are free)

Further LP problems:

sc50a (sc50a_c are the constraints and sc50a_t is the objective function)
Same for sc50b. One out of sc50a and sc50b should be significantly easier than the other

Automatically prove the following:

Consider the infinite sequence (x_n) of real numbers defined by x_i+2 = |x_i+1| − x_i, where x₁ and x₂ are arbitrary numbers. Then (x_n) is periodic with period 9.