Haniel Barbosa authored 11 months ago and Lachnitt committed 11 months ago

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Hans-Jörg authored 11 months ago and Lachnitt committed 11 months ago

Co-authored-by: Hans-Jörg <commits@schurr.at>

Addresses #37

Adresses #35

Addresses #36

This follows the advice given here:
https://latex.org/forum/viewtopic.php?t=32205
The option changes how destination names are defined.

Also fixes two other small typos related to references.

Should address:
#39

Addresses #40

- adress normalizing of terms with context push (and other typos)
- Remark on missing Gamma

- replace semantic by semantics
- apply some review suggestions

The simplification `(P -> Q) -> Q => P or Q` is already covered
by `bool_simplify`.

- Define what a valid Alethe proof is formally
- Show that a valid Alethe proof is sound
- TODO: nicer handling of let

It was used in a few places to represent complementary literals,
but is mostly used to represent vectors of terms, variables.  This
commit removes the usage for complementary literals.  The few
places that used it now define the complement manually.

It's n-ary.