1. Uses a form of symbolic logic. 16.2
1.1. declarative languages
1.1.1. declares semantics
1.1.2. Nonprocedural
1.1.2.1. form of result
2. Prolog 16.5-16.7
2.1. Origins
2.1.1. University of Edinburgh
2.1.1.1. Kowalski
2.1.2. University of Aix-Marseille
2.1.2.1. Calmerauer & Roussel
2.2. Variables
2.2.1. sequence of letters and digits, beginning with a capital letter
2.2.1.1. unknowns in algebra
2.2.1.2. tries to find variable values that allow clause to succeed
2.2.1.2.1. Later code cannot change variable value
2.2.1.2.2. can backtrack and change variable value if clause cannot be satisfied
2.2.2. Not bound to types by declarations
2.2.2.1. The binding of a value, and thus a type, to a variable is called an instantiation. Instantiation occurs only in the resolution process.
2.2.2.2. A variable that has not been assigned a value is called uninstantiated
2.3. Rule Statements
2.3.1. Conjunctions
2.3.1.1. Multiple terms separated by (AND) operations
2.3.1.2. consequence :- antecedent_expression
2.4. Goal Statements
2.4.1. proposition to prove or disprove
2.5. Fact Statements
2.5.1. Assumed to be true
2.5.2. Can store in database
2.5.3. headless Horn clause
2.5.3.1. statements from which new information can be inferred
2.5.4. Rules are generalized and must be followed to a tee to be considered true
2.5.4.1. Antecedent (then clause)
2.5.4.2. Consequent (if clause)
2.5.5. Facts are always true
2.6. List Structures
2.6.1. Sequences of any number of elements
2.6.1.1. Elements can be atoms, atomic propositions, or any other terms, including lists
3. Predicate Calculus 16.3
3.1. Express propositions.
3.1.1. Propositions - Logical statement that may or may not be true
3.1.1.1. constants and variables
3.1.1.1.1. Atom - String of letters, digits, and underscores beginning with a lowercase letter
3.1.1.2. Compound propositions
3.1.1.2.1. Two or more atomic propositions connected by operators
3.2. Express relationships between propositions
3.2.1. Clausal Form/rule
3.2.1.1. A conclusion can be drawn if a given set of conditions is satisfied
3.2.1.2. Headed Horn Clause
3.2.1.2.1. Antecedent: right side (if part)
3.2.1.2.2. Consequent: left side (then part)
3.3. Infer new propositions from existing ones
3.3.1. Resolution
3.3.1.1. Theorem proving - basis for logic programming
3.3.1.2. Allows inferred propositions to be computed from existing ones.
3.3.1.2.1. steps
4. 16.8 Applications of Logic Programming
4.1. Expert Systems
4.1.1. Computer systems designed to emulate human expertise in some particular domain.