Logical Entailment and Reasoning
Set of premises DELTA, logically entails a conclusion ETA iff every interpretation that satisfies the premises also satisfies the conclusion. The sign for logical entailment is "|="
- Do a truth table to see if premise logically entails conclusion. 
Formalization and automation 
Why we want to learn about logic and automated reasoning. Applications are boundless.
Valid vs Contingent vs Unsaatisfiable
Valid - all truth assigments work 
Contingent - at least one true and one false. 
Unsatisfiable - none given true 
Satisfiable - possible to be true
Falsiable - possible to be false
Empty disjunction/conjunction 
Disjunction of no literals (AKA a clause containing no literals) is FALSE. 
HOWEVER empty conjunction is TRUE.
Logical Equivalence
NOT THE SAME as logical entailment. 
For two sentences to be logically equivalent, every truth assignment that satisfies of first sentence must satisfy second sentence. AND vice versa. 
Logical Consistency
For two sentence to be logically consistent, there must be AT LEAST ONE truth assignment that satisfies both sentences. 
Relational vs Propositional Logic
Similarities: same precedence, same rules for logical sentences 
Differences: Relational is more general. Doesn't have propositional variables, instead has:
- object constants (use letters at the beginning of the alphabet)
- relational constants (arity = # of arguments)
- variables (use letters at the end of the alphabet)
Propositional Logic
Propositional variables: either TRUE or FALSE propositional constants. I.e.  In p -> q, p and q are propositional variables. 
Propositional/Relational Logic -
Operator Precedence (highest to lowest)
Quantifiers (forall, there exists)
Not
And
Or
Implies, IFF
Ground, Free, Open, Instance
Ground sentence - sentence of no variables (all constants)
Ground term - AKA object constants
Free - variable that isn't quantified (i.e. in the scope of a quantifier). If it is, then it's bound.
Open - sentence that has free variables; if not, then closed.
Instance of an expression: all free variables have been consistently replaced by ground terms.
Herbrand Base
Set of all ground relational sentences that can be formed from the constants of the language. 
Relational Logic
Truth Assignment
Maps each sentence in Herbrand base to truth value.
Satisfaction
Truth assignment i satisfies a sentence with free variables iff it satisfies every instance of that sentence. 
Set of sentences satisfaction
Truth assignment i must satisfy all sentences.
- To check, build truth table 
Logical Entailment
A set of sentences T logically entails sentence O iff every truth assignment that satisfies T also satisfies O. 
- A sentence with free variables is equivalent to the sentence in which all free variables are universally quantified. 
Going from RL to PL
1) Convert sentence to prenex form (rename variables in different quantified sentences to eliminate any duplicates, and then apply quantifier distribution rules in reverse to move quantifiers outside of logical operators)
2) Compute the grounding (basically if a sentence is ground, just add it to PL set of sentences, else if it has existential/universially quanitified then add the corresponding ground sentences) 
3) Replace the relational constants with propositional constant. 
New Note
General Relational Logic
Evaluation/satisfaction/logical entailment
Obviously, not practical, since truth assignments are infinite.
General Relational vs Relational 
Similarities: relational sentences, logical sentences, quantified sentences all defined exactly the same. 
Differences: General is more general. Adds
- functional constants (like relational constants, has arity). Return value is object constant (instead of propositional constant). Ex. f(a,y), where f is functional constant and arity is 2. 
- functional expressions/term (the entire expression). Can be nested. Ex. f(a,y). f(f(a)). 
Key difference
Herbrand base is infinite. Thus, any truth assignment is necessarily infinite. 
Universal Introduction
If the variable being quantified appears in the sentence being quantified, it must not appear free in any active assumption. 
- But you can add it to your sentence using Implication Introduction, and then it's okay.
Universal Elimination
Allows us to reason from general to the particular. 
Existential Introduction
If sentence involves a ground term t, then we can EI.
Existential Elimination
(analogous to Or Elimination)
Power of Free Variables
We can manipulate them as though we are talking about specific individuals (although each one could be any object); and, when we're done, we can universalize them to derive universally quantified conclusions. 
General Relational Logic Proofs
Relational Resolution Principle
Both sound and complete for all of Relational Logic.  Key differences from prop resolution:
- Rename variables before doing unification. 
- Use unification to unify literals before applying the rule, which is same as propositional resolution. 
Relational Resolution
Clausal Form
A clause is a set of literals and represents a disjunction of the literals in a set. 
A clause set is a set of clauses, representing the conjunction of classes in the set.
Steps to put in clausal form
INSEADO
1) Implications out 
2) Negations in
3) Standardize variables. Rename variables so that each quantifier has a unique variable (the same variable is not quantified more than once within same sentence).
4) Existentials out. A bit complicated. There are two cases: 
    1) quantifier does not occur within scope of universal quantifier. Simply remove variable, replace with Skolem constant (MUST BE FULLY UNIQUE). 
    2) if it does, then replace with Skolem function instead (MUST BE FULLY UNIQUE). 
5) Drop all universal quantifiers.
6) Disjunctions in 
7) Operators out 
Unification
Processing of determining whether two expressions can be unified (made identical by appropriate substitutions for their variables).
- Iterate through expresssions. If same constants, move on
Substitutions
Pure iff all replacement terms in range are free of variables in domain of substitution. Otherwise, impure. 
Composition of multiple substitutions is straightforward (just combine effects). Does not preserve purity. Composability = preserves purity.
A substitution S is more general than another S' substitution if Sp = S' (where p is another substitution).
In resolution, we are interested in unifiers that are most general unifiers. 
Overall
Like propositional resolution, relational resolution is sound, but not generatively complete (that is, we can't find resolution derivations of all clauses that are entailed by any set of premises, including empty set of premises).
- For example, given an empty set of premises, you can't prove anything, even though it entails everything. 
Soundness vs Compleness
Sound if, every provable conclusion is logically entailed.
Complete if, every conclusion that's logically entailed is provable.
Fitch is BOTH sound and complete for propositional logic.
Mendelson is BOTH sound and complete for premises & conclusions that can be written with ~ and =>.
Mendelson
Only 4 rules:
- Implication introduction
- Implication elimination
- Implication distribution
- Contradiction realization
Logical Entailment
Show that adding the negation of sentence being tested, to the set of sentences, is unsatisfiable.
Propositional Logic
   Login to remove ads X
Feedback | How-To