Term
| General convert KB to Conjunctive Normal Form (CNF) |
|
Definition
- Functions are eliminated
- All quantifiers are eliminated
- Result is in clausal form |
|
|
Term
|
Definition
1. Eliminate implication
2. Reduce scope of not to single terms
3. Standardize variables
4. Eliminate existential quantifiers
5. Move quantifiers to left (prenix normal form)
6. Drop prefix
7. Convert into conjunctions of disjuncts
8. Write as a set of separate clauses, one per conjunct
9. Rename variables so each clause has unique variables |
|
|
Term
| Basic components of First Order Logic (FOL) |
|
Definition
1. Objects
2. Relations among objects
3. Functions |
|
|
Term
|
Definition
- Represents a possible world
- A model contains a set of objects |
|
|
Term
|
Definition
- Functions in FOL are all total functions
- Total functions return an object for all sets of arguments |
|
|
Term
|
Definition
An expression that refers to domain elements (constant symbols, variable symbols, or function expressions).
A "ground term" has no variables in it |
|
|
Term
|
Definition
| AKA Well Formed Formuli (wff), sentences represent truth values. |
|
|
Term
DeMorgan's Law for Quantifiers:
[image] |
|
Definition
|
|
Term
DeMorgan's Law for Quantifiers:
[image] |
|
Definition
|
|
Term
DeMorgan's Law for Quantifiers:
[image] |
|
Definition
|
|
Term
DeMorgan's Law for Quantifiers:
[image] |
|
Definition
|
|
Term
|
Definition
- An alternative semantics intended to simplify representation
-Includes the following:
- Unique names assumptions
- Closed world assumption - Atomic sentences whose truth values are not known are assumed to be false
- Domain closure - The only objects in the domain are those named by constants |
|
|
Term
|
Definition
| A basic fact, that MAY represent a definition. Simple facts, however, are often expressed by atomic sentences, which are NOT definitions. |
|
|
Term
|
Definition
| Specifies equivalence between two facts using a biconditional or logical equivalence. Definitions are a subset of axioms |
|
|
Term
|
Definition
| Anything inferred from the KB. Adding theorems does not add new information, but they decrease the amount of inference required to perform later inferencing. |
|
|
Term
|
Definition
| An axiom that cannot be derived from others |
|
|
Term
|
Definition
| Used to add knowledge to the KB. These statements are called assertions. |
|
|
Term
|
Definition
| Used to ask a question of a KB. Will return true or false. |
|
|
Term
|
Definition
| Asks a question of the KB, then returns a binding list or substitution of the form {var/binding}. |
|
|
Term
| Inferencing in FOL vs propositional logic |
|
Definition
| Very similar, except FOL must account for quantification |
|
|
