96
Formal Logic
o n t H e c o M P u t e R
For Exercises 1–5, write a computer program that produces the desired output from the given input.
1. Input: Truth values for two statement letters A and B
Output: Corresponding truth values (appropriately
labeled, of course) for
A ` B, A ~ B, A S B, A 4 B, A′
2. Input: Truth values for two statement letters A and B
Output: Corresponding truth values for the wffs
A S B′ and B′ ` [A ~ (A ` B)]
3. Input: Truth values for three statement letters A, B,
and C
Output: Corresponding truth values for the wffs
A ~ (B ` C′) S B′ and A ~ C′ 4 (A ~ C )′
4. Input: Truth values for three statement letters
A, B, and C, and a representation of a simple
propositional wff. Special symbols can be used for
the logical connectives, and postfix notation can be
used; for example,
A B ` C ~ for (A ` B) ~ C
or
A′ B ` for A′` B
Output: Corresponding truth value of the wff
5. Input: Representation of a simple propositional wff
as in the previous exercise
Output: Decision on whether the wff is a tautology
6. Using the online Toy Prolog program that can be
found at http://www.csse.monash.edu.au/~lloyd/
tildeLogic/Prolog.toy, enter the Prolog database of
Example 39 and perform the queries there. Note
that each database entry requires a period. Also add
the recursive rule for infoodchain and perform the
query
?infoodchain(bear, Y )
section 1.3
1. A predicate wff that begins with a universal
quantifier is universally true, that is, true in all interpretations.
2. In the predicate wff (4x)P(x, y), y is a free variable.
3. An existential quantifier is usually found with the
conjunction connective.
4. The domain of an interpretation consists of the
values for which the predicate wff defined on that
interpretation is true.
5. A valid predicate wff has no interpretation in which
it is false.
section 1.4
1. The inference rules of predicate logic allow existential and universal quantifiers to be added or
removed during a proof sequence.
2. Existential instantiation should be used only after
universal instantiation.
3. P(x) ` (E x)Q(x) can be deduced from (4x)
[P(x) ` (E y)Q( y)] using universal instantiation.
4. Every provable wff of propositional logic is also
provable in predicate logic.
5. A predicate wff that is not valid cannot be proved
using predicate logic.
section 1.5
1. A Prolog rule describes a predicate.
2. Horn clauses are wffs consisting of single negated
predicates.
3. Modus ponens is a special case of Prolog resolution.
4. A Prolog recursive rule is a rule of inference that is
used more than once.
5. A Prolog inference engine applies its rule of inference without guidance from either the programmer
or the user.
section 1.6
1. A provably correct program always gives the right
answers to a given problem.
2. If an assertion after an assignment statement is
y > 4, then the precondition must be y ≥ 4.
3. Proof of correctness involves careful development
of test data sets.
4. Using the conditional rule of inference in proof
of correctness involves proving that two different
Hoare triples are valid.
5. The assertions used in proof of correctness can also
be used as a program design aid before the program
is written, and as program documentation.
Formal Logic
o n t H e c o M P u t e R
For Exercises 1–5, write a computer program that produces the desired output from the given input.
1. Input: Truth values for two statement letters A and B
Output: Corresponding truth values (appropriately
labeled, of course) for
A ` B, A ~ B, A S B, A 4 B, A′
2. Input: Truth values for two statement letters A and B
Output: Corresponding truth values for the wffs
A S B′ and B′ ` [A ~ (A ` B)]
3. Input: Truth values for three statement letters A, B,
and C
Output: Corresponding truth values for the wffs
A ~ (B ` C′) S B′ and A ~ C′ 4 (A ~ C )′
4. Input: Truth values for three statement letters
A, B, and C, and a representation of a simple
propositional wff. Special symbols can be used for
the logical connectives, and postfix notation can be
used; for example,
A B ` C ~ for (A ` B) ~ C
or
A′ B ` for A′` B
Output: Corresponding truth value of the wff
5. Input: Representation of a simple propositional wff
as in the previous exercise
Output: Decision on whether the wff is a tautology
6. Using the online Toy Prolog program that can be
found at http://www.csse.monash.edu.au/~lloyd/
tildeLogic/Prolog.toy, enter the Prolog database of
Example 39 and perform the queries there. Note
that each database entry requires a period. Also add
the recursive rule for infoodchain and perform the
query
?infoodchain(bear, Y )
section 1.3
1. A predicate wff that begins with a universal
quantifier is universally true, that is, true in all interpretations.
2. In the predicate wff (4x)P(x, y), y is a free variable.
3. An existential quantifier is usually found with the
conjunction connective.
4. The domain of an interpretation consists of the
values for which the predicate wff defined on that
interpretation is true.
5. A valid predicate wff has no interpretation in which
it is false.
section 1.4
1. The inference rules of predicate logic allow existential and universal quantifiers to be added or
removed during a proof sequence.
2. Existential instantiation should be used only after
universal instantiation.
3. P(x) ` (E x)Q(x) can be deduced from (4x)
[P(x) ` (E y)Q( y)] using universal instantiation.
4. Every provable wff of propositional logic is also
provable in predicate logic.
5. A predicate wff that is not valid cannot be proved
using predicate logic.
section 1.5
1. A Prolog rule describes a predicate.
2. Horn clauses are wffs consisting of single negated
predicates.
3. Modus ponens is a special case of Prolog resolution.
4. A Prolog recursive rule is a rule of inference that is
used more than once.
5. A Prolog inference engine applies its rule of inference without guidance from either the programmer
or the user.
section 1.6
1. A provably correct program always gives the right
answers to a given problem.
2. If an assertion after an assignment statement is
y > 4, then the precondition must be y ≥ 4.
3. Proof of correctness involves careful development
of test data sets.
4. Using the conditional rule of inference in proof
of correctness involves proving that two different
Hoare triples are valid.
5. The assertions used in proof of correctness can also
be used as a program design aid before the program
is written, and as program documentation.