Proof Generator

A logical formula is built from the grammar in Figure 1(a). A variable stands for a truth value; (+F1...Fn) is the logical disjunction of the formulae Fi; (*F1...Fn) is their logical conjunction; and ~F is the negation of F. A formula that matches the grammar in Figure 1(b) is said to be in ACM Normal Form (ACMNF).

<formula>  ::= <variable> | ~<formula> | (+<formulae>) | (*<formulae>)
<variable> ::= a lower-case letter of the English alphabet
<formulae> ::= <formula> | <formula><formulae>

Figure 1(a). General syntax of a formula

<ACMNF_formula> ::= <term> | (+<terms>)
<term>          ::= <literal> | (*<literals>)
<terms>         ::= <term><term> | <term><terms>
<literal>       ::= <variable> | ~<variable>
<literals>      ::= <literal><literal> | <literal><literals>
<variable>      ::= a lower-case letter of the English alphabet

Figure 1(b). ACMNF syntax of a formula

A formula is converted to ACMNF with the rewriting rules below, where F is a formula, S is a non-empty sequence of formulae, and s, s' are possibly empty sequences of formulae. Applying a rule q → r means replacing a part matching pattern q with r, as in Figure 2. Rewriting stops when no rule applies. It always terminates, and the result is unique regardless of the order in which the rules are applied.

1. ~~F → F
2. ~(*FS) → (+~F~(*S))
3. ~(+FS) → (*~F~(+S))
4. (+F) → F
5. (+s(+S)s') → (+sSs')
6. (*F) → F
7. (*s(*S)s') → (*sSs')
8. (*s(+FS)s') → (+(*sFs')(*s(+S)s'))

(+(*(+~(*ab)) (+~a) )c)    -4→
(+(*(+ ~(*ab) )~a)c)       -2→
(+(* (+(+~a~ (*b) ))~a)c)  -6→
(+(* (+(+~a~b)) ~a)c)      -4 or 5→
(+ (*(+~a~b)~a) c)         -8→
(+(+(*~a~a)(* (+~b) ~a))c) -4→
(+(+(*~a~a)(*~b~a))c)      -5→
(+(*~a~a)(*~b~a)c)

Figure 2. Converting a formula to ACMNF

A set of axioms is a list (V1 V2 ... Vn) of the variables that are true; every variable not in the list is false. A proof of a formula F under a set of axioms A is a term of the ACMNF of F that is true under A. For example, the terms (*~a~a) and c are the proofs of (+(*(+~(*ab))(+~a))c) under the axioms (bc).

Build a proof generator that, given a formula F, a set of axioms A, and a number k, outputs the next k proofs of F in the order in which they appear in the ACMNF of F. When the proofs are exhausted, generation continues again from the first proof. For instance, the first proof of (+(*(+~(*ab))(+~a))c) under (bc) is (*~a~a); generating three more proofs yields c, (*~a~a), and c. If the ACMNF contains identical terms, each occurrence is considered a distinct term.

The input consists of several data sets and is terminated by end of file. Each data set has the form

F A k1 ... kn 0

with n > 0, where F is a formula, A is a set of axioms, and k1 ... kn are long integers, none equal to 0. The value 0 marks the end of the data set. White space may appear freely between tokens. A formula has at most 500 characters, and every ACMNF term is at most 80 characters long, not counting white space. All input is guaranteed to be well formed.

For each data set, keep a single running cursor over the proofs of F and process the ki in order. For each ki (i = 1 ... n), generate the next |ki| proofs of F, advancing the cursor cyclically. If ki > 0, print those |ki| proofs; if ki < 0, advance the cursor without printing anything. Each printed proof begins at the start of its own line and contains no white space between its characters.