308-424 (Topics in Artificial Intelligence as taught by G. Dudek)
A set of wffs connected by AND's is a conjunction.
A set of wffs connected by OR's is a disjunction.
Variable P : associated literals are P and ¬ P.
We attach meaning to wwfs in 2 steps:
1. By assigning truth values to the propositional variables
2. By associating real-world concepts with symbols
Step 1, assigning truth values, is called an interpretation.
Step 2 is called symbol grounding, and is not related to the logical consistency or mathematical soundness of the logical system.
The purely logical aspects of propositional logic should be familiar to CS students. You should read sections 3.1 and 3.2 of the textbook to assure you know the correct terminology and concepts.
A particular set of truth assignments associated with propositional variables is a model IF THE ASSOCIATED FORMULA (or formuli) come out with the value true.
For the formula
(A and B) implies ( C and D) the assignment
A=true B=true C=true D=true is a model.
The assignment
A=false B=true C=true D=true is another model, but the assignment
A=true B=true C=true D=false is not a model.
If *no model is possible * for a formula, then the formula is NOT SATISFIABLE, otherwise it is satisfiable.
A Theory is a set of formuli (in the context of propositional logic).
If no model is possible for the negation of a formula, then we say the original formula is valid.
If a formula is always true, it is a tautology.
An axiom is a wff that states a priori information.
Proper axioms state facts.
An axiom schema is a formula (but NOT a wff), in which
It uses schema variables to represent wffs: i.e. it is a form to be filled in.
Logical axioms, expressed as axiom schemas, express how to derive further truths.
The set of proper axioms that encode information about a specific domain is called a domain theory.
An example:
| Domain theory for McGill entrants |
(smart AND goes-to-school) IMPLIES good-student (adventurous AND smooth) IMPLIES successful montrealer EQUIV-TO (smart AND (nice OR adventurous) cs-major EQUIV-TO (smart OR adventurous) roboticist EQUIV-TO (adventurous AND creative) nerd IMPLIES (NOT adventurous) |
There are usually many ways of expressing the same thing.
A canonical form (or normal form) is a standard way for constructing wffs.
Using a canonical from makes it much easier to code-up an inference program.
The most standard is the conjunctive normal form (CNF): every wff is made up of a conjunction of either literals or disjunctions. i.e. (a OR b OR c OR d ...).
Disjunctive normal form is another standard approach.
e.g.:
Rule-based expert systems use rules to make inferences or decide what to do. Where are often expressed as Horn clauses, a special type of CNF with all the literals EXCEPT ONE negated: