Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.

documentation → tutorials → propositional

Tutorial 1: Basic Propositional Logic — 20 min

Propositional logic is one of the simplest logical formalisms, which makes a good starting point to get into Redlog.

Domain Selection

Reduce (Free CSL version), 19-Aug-15 ... 1: rlset boolean; *** turned off switch lower {}{} 2: on rlpcprint;

We use rlset to select the relevant domain, which is called boolean. We could also have used its short name B. As a side effect, rlset has auto-loaded the Redlog package and the relevant domain modules. Functions with one argument do not require parentheses. On the other hand, functions with no arguments require an empty pair of parentesis.

The printed message indicates that Reduce has been put into case-sensitive mode. Note that 3 asterisks "***" indicate an informative message. In contrast, 5 asterisks "*****" would indicate an error. The return value of rlset is the previous domain, which is empty here, because we just started in a fresh session.

Turning on the switch rlpcprint will allow us to use upper case letters as propositional variables and to ignore the formal construction of propositional logic on the basis of the underlying first-order framework with our first steps here.

Formula Input

3: phi := A or A and B and C; phi := A or (A and B and C)φ := A ∨ (A ∧ B ∧ C) 4: psi := phi or B and not C and D or false; psi := (A or (A and B and C)) or (B and not(C) and D) or falseψ := (A ∨ (A ∧ B ∧ C)) ∨ (B ∧ ¬ (C) ∧ D) ∨ false

With the definition of phi notice that the operator and takes precedence over the operator or. The existing formula phi is reused for defining psi. It is important to understand that the propositional constants and operators serve as constructors. There are no implicit logical simplifications. Nevertheless some evaluation takes place here. For instance, redefining phi would not affect the existing psi.

Counting and Analyzing

5: length psi; 3 6: part(psi, 1, 2); A and B and C 7: rlatnum psi; 7 8: rlatl psi; {A,B,C,D} 9: rlatml psi; {{A,2},{B,2},{C,2},{D,1}}

The length of a formula is the number of arguments of its toplevel operator, which is or here. Since length is a standard Reduce function, it is not prefixed with "rl."

The function part takes an arbitrary number of arguments, which give the path to a subformula. The path can end with \(0\), which denotes the corresponding operator.

rlatnum counts the number of atoms with multiplicities, which is quite a good measure for the size of a formula. rlatl gives the list of atoms without multiplicities, while rlatml returns a multiplicity list associating with each atom the number of its occurrences.

Normal Forms and Simplification

10: rlsimpl psi; A or (B and not(C) and D) 11: rlcnf psi; (A or B) and (A or not(C)) and (A or D) 12: rlnnf not(A and B or not(not C and D)); (not(A) or not(B)) and (not(C) and D)

In all domains rlsimpl is the standard simplifier. While for some domains sophisticated simplification techniques might not terminate within reasonable time, rlsimpl generally provides a good tradeoff between efficiency and quality of results. In our example the output happens to be in disjunctive normal form.

rlcnf explicitly computes a conjunctive normal form. Such normal form computations, like many other Redlog functions, implicitly apply the standard simplifier in the end. Of course, there is also rldnf available. rlnnf computes a negation normal form moving all logical negations towards the atoms.

Satisfiability and Quantifier Elimination

13: rlqe rlex psi; true 14: rlqe rlall psi; false 15: rlqe all(a, ex(b, all({c, d}, psi))); false 16: rlqe all(a, ex(b, psi)); not(C) and D

We first solve a classical satisfiability (SAT) problem by using the existential closure rlex to existentially quantify all variables occurring in psi and then applying quantifier elimination to compute a quantifier-free equivalent. Analogously, universal quantification can be used to decide validity without explicit reduction to satisfiability via negation.

We can also solve quantified Boolean formula (QBF) problems by making the quantification explicit using the first-order quantifiers ex and rlall. Their first argument is either a variable or a list of variables, which is expanded into several nested quantifiers. The quantifiers require the variables in their first argument to be lower case while the propositional variables establishing atoms must be upper case. Let us not go into detail about this here.

Finally, we can go beyond QBF by even leaving some variables unquantified. The elimination result is then not necessarily true or false but a necessary and sufficient condition in those unquantified variables.

References

  1. A. Seidl and T. Sturm. Boolean quantification in a first-order context. Proc. CASC 2003. Technische Universität München, Germany, 2003.
  2. T. Sturm and C. Zengler. Parametric quantified SAT solving. Proc. ISSAC 2010. ACM Press, 2010.