ACE Coursework 2
Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit
ACE Coursework 2
1. Problem Specification
Every formula 
of propositional logic can be converted into another formula 
′ such that 
and 
′ are logically equivalent, and where 
′ is a disjunction of conjunctions of literals, where a literal is either an atom or its negation. We say that 
′ is in disjunctive normal form (DNF). For example, in the propositional case, a DNF formula looks like this:
(
∧ ¬
) ∨ (
∧ 
∧ ¬
∧ 
) ∨ (¬
∧ 
)
Let 
be a finite set of individual names. The syntax of the logic of direction (LD) is defined as 
, 
≔ 
(
, 
) | 
(
, 
) | 
(
, 
) | 
(
, 
) | 
(
, 
) | 
(
, 
) | ¬
| 
∧ 
Where 
, 
∈ 
, 
∨ 
= ¬(¬
∧ ¬
) , 
→ 
= ¬(
∧ ¬
), 
↔ 
= (
→ 
) ∧ (
→ 
), ⊥= 
∧ ¬
, ⊤ = 
∨ ¬
.
Write a Java program that takes an LD formula 
, which does not involves ↔, as input, and outputs another formula 
′ such that 
and 
′ are logically equivalent and 
′ is in DNF.
2. Input and Output
The inputs and outputs are both Java Strings. The following table shows how to represent each logical operator as a String in Java.
|
Standard logical operator |
Corresponding symbol as a String in Java |
|
¬ |
~ |
|
∧ |
& |
|
∨ |
| |
|
→ |
-> |
We use “T” and “F” to represent ⊤ and ⊥ respectively.
To simplify the problem, we define the input format of an LD formula as follows: A formula is an atomic formula or a complex formula.
An atomic formula is of one ofthe forms:
, 
, 
(
, 
), 
(
, 
), 
(
, 
), 
(
, 
), 
(
, 
), 
(
, 
).
A complex formula is of one ofthe forms:
~ [ 
]
[ 
] & [ 
]
[ 
] | [ 
]
[ 
] -> [ 
]
Sample inputs and outputs are provided as follows.
|
Input |
Output |
|
~ [ [ E(a,b) ] & [ W(b,c) ] ] |
~ [ E(a,b) ] | ~ [ W(b,c) ] |
|
[ E(a,b) ] -> [ W(b,c) ] |
~ [ E(a, b) ] | [ W(b,c) ] |
|
[ E(a,b) ] & [ ~ [ E(a,b) ] ] |
F |
|
[ E(a,b) ] | [ ~ [ E(a,b) ] ] |
T |
For more examples, see examples.txt.
3. A Standard Procedure
For your reference, a standard procedure to convert an LD formula, which does not involve ↔, into DNF is as follows. You may follow this procedure, or follow any other procedure, as long as it works correctly.
(1) Eliminate →, using the following equivalence: 
→ 
≡ ¬
∨ 
(2) Move ¬ inward so that it appears only in front of an atom, using the following equivalences:
¬¬
≡ 
¬(
∧ 
) ≡ (¬
∨ ¬
)
¬(
∨ 
) ≡ (¬
∧ ¬
)
(3) Distribute ∨ over ∧, using the following equivalences:
(
∧ (
∨ 
)) ≡ (
∧ 
) ∨ (
∧ 
)
((
∨ 
) ∧ 
) ≡ (
∧ 
) ∨ (
∧ 
)
(4) Collect terms, using the following equivalences:
(
∨ 
) ≡ 
(
∧ 
) ≡ 
(
∨ ¬
) ≡ ⊤
(
∧ ¬
) ≡⊥
¬(⊤) ≡⊥
¬(⊥) ≡ ⊤
⊤ ∨ 
≡ 
∨ ⊤ ≡ ⊤
⊤ ∧ 
≡ 
∧ ⊤ ≡ 
⊥ ∨ 
≡ 
∨ ⊥ ≡ 
⊥ ∧ 
≡ 
∧ ⊥ ≡ ⊥
4. Coursework Submission
Please submit a zip file which consists of:
Java program files;
a “read me” file describing the structure of your Java program and how to run your program;
a report (in PDF format) briefly describing how you solved the given problem, including
which data structure you used and why, the algorithms designed and implemented, and why your program works correctly, time complexity of the program, the testing of your program, etc. Keep the report short and brief, within 2-3 pages.
Keep your code and report brief and clear! Good luck! 
2021-12-04