Codah ClubTrain. Submit. Improve.
Sign in
English
#0004B0

seerc-2010-i

A logical formula has the syntax shown in figure 1(a), where a variable stands for a truth value, the formula (+F1...Fn) stands for the logical disjunction of the formula Fi, (* F1...Fn) denotes the logical
conjunction of the formula Fi, and ~F is the negation of F. If a formula has the particular syntax given in figure 1(b) we say that the formula is in the ACM Normal Form (ACMNF).


Image: slika1

A formula is converted to ACMNF using the rewriting rules given below, where F represents a formula, S stands for a non empty sequence of formulae, and s and s' denote possibly empty sequences of formula. Applying a rewriting rule q→r on a formula F means to substitute by r a part of F that matches the pattern q, as in shown figure 2. The conversion terminates when no rewriting rule can be applied. The conversion terminates for any formula, and the result is unique regardless which rules are applied on which parts of the formula and in which order.


Image: slika2

A set of axioms is represented as a list (V1 V2...Vn) of variables that are true. A variable that is not in the list is false. A proof of a formula F according to a set of axioms A is a term from the ACMNF of F such that the term is true according to A. For instance, the terms (*~a~a) and c are the proofs of the formula (+(*(+~(*ab))(+~a))c) according to the axioms (bc).


The problem is to code a proof generator that for a given 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. If the proofs are exhausted, the generator continues from the first proof of F. For example, generating the first proof of the formula (+(*(+~(*ab))(+~a))c) according to the axioms (bc) yields (*~a~a). Generating three more proofs produces c, (*~a~a), and c. If the ACMNF of a formula contains similar terms, as in the last
example in figure 3, these terms are considered distinct.


Image: slika3

InputWrite a proof generator that reads sets of data from the standard input. The content of a data set is F A k1...kn 0, n>0, where F is a formula, A is a set of axioms, and k1...kn are long integers different than 0. For each ki, i=1,n, the program generates the next |ki| proofs of F and, if ki>0, prints these proofs on the standard output.

OutputEach printed proof starts from the beginning of a line and there are no white spaces between the characters of the proof. The generated proofs are not printed if ki>0. White spaces are used freely in the input. A formula has at most 500 characters and a ACMNF term is at most 80 characters long, not counting white spaces. The input data terminate with an end of file, and are correct.

Submit solution

Coming later

The grading service will be connected in a later migration step. You can inspect the task and your previous results now.