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 

