(evtl. autotool) bestimme wfmAs für
- Peano-Multiplikation (Variante A: ohne Additionsregeln, B: mit)
- symbolisches Differenzieren
-
{p∧(q1∨q2)→(p∧q1)∨(p∧q2),
(p1∨p2)∧q→(p1∧q)∨(p2∧q)}
.
beweise:
- das Verifikationsproblem für lineare Interpretationen
(über
, über
d
) ist entscheidbar
- das Syntheseproblem für lineare Interpretationen
mit Anstieg 1 (d.h.
[f](x1,…, xk) = x1 + … + xk + cf
) ist entscheidbar.
Johannes Waldmann
2015-12-11