## Logic ### Basics - Logics are the basics of deductive databases - How to generate knowledge? 1. *Axioms*: Start with knowledge which is considered true 2. *Inference*: Derive new knowledge - **Types of inference**: - Inductive Inference: - Draw conclusions from multiple observations - e.g., natural science - Deductive Inference: - Axioms are given - Generate conclusions (theorems) from true facts (axioms) using rules - *Focus of this lecture* #### History - Sophism - 5th century BC - *Sophists* were like teachers - Teach rhetoric for money - Try to convince people using fallacious reasoning - Use ambiguities of languge - Aristotle - 330 BC - First appearance of formal logics - Goal: - Derive new knowledge from old knowledge - Formal and safe inference - Logic as *tool* for valid philosophical arguments - Discovered Sophists' tricks - Fallacy of Equivocation - *Feather is light. Light can not be dark. A feather can not be dark.* - Fallacy of Composition - *Each individual vote is rational. Therefore, combining multiple votes is rational.* - Fallacy of Accident - *Cutting people with knives is a crime. Surgeons cut people with knives. Surgeons are criminals.* - Fallacy of Begging the Question #### Other Logics ##### Propositional Logic - Often referred as *zero-order logic* - Components: - *Atomic statement*: Statement that can not be further divided (true of false) - *Connectives*: AND, OR, IMPLICATION (truth function) - Bivalent logic - Only *true* and *false* - Counterpart of multi-valued logics (e.g., Fuzzy logic) - 400 BC: Aristotle - Wrote the book *Metaphysics* - Base of propositional logic - *A statement AND its contradiction can not be true at the same time.* - *A statement OR its contradiction has to be true.* - Invented the technique of indirect proofs - 1847: George Boole - First *sound* and *complete* formalization for truth values with algebraic calculus - Invented *Boolean Algebra* - Graphic representation by Venn diagrams - 1879: Gottlob Frege - Formalized first calculus with implications - 1910: Bertrand Russel - Refine Frege's calculus - Problems: - Does not investigate the statements themselves - e.g., for with variables does the statement hold - Bad for deductive databases - No quantifiers/predicates ##### Term Logic - Introduced by Aristotle - Purpose: Allow deductive inference ###### Constructs - **Term**: - Word represents *something* - Has no truth value - Just objects (e.g., man, blue) - **Proposition**: - Combination of two terms - Truth value: Either true or false - Have *Quantity*: - Universal (*all*) - Existential/Particular (*some*) - Have *Quality*: - Affirmative (e.g., *is*) - Negative (e.g., *is not*) - Combinations: - Universal affirmative (UA): `$ \forall $` - Existential affirmative (PA): `$ \exists $` - Universal negative (UN): `$ \neg\forall $` - Existential negative (PN): `$ \neg \exists $` - **Syllogism**: - *Inference* where a proposition (*conclusion*) follows two other propositions (*premise*) - `$ \text{Minor premise} \land \text{Major premise} \Rightarrow \text{Conclusion} $` - Components: - *Minor premise*: Contains a minor term and and middle term - *Minor term*: Subject - *Middle term*: Predicate - *Major premise*: Contains the middle term and the major term - *Middle term*: Subject - *Major term*: Predicate - *Conclusion*: Contains the minor term as subject and the major term as predicate - Important: The middle term must appear as predicate and as subject ###### Inference - Example (UA-UA-UA): - Minor premise: All Greeks (subject) are men (predicate). - Major premise: All men (subject) are mortal (predicate). - Conclusion: All Greeks are mortal. - Results in 24 valid types of syllogisms - Based on allowed conversations - UA-UA-UA - UN-UA-UN - PN-UA-PN - etc. - *Square of opposition*: - Allow for logical conversions - UA is contradiction of PN - PA is contradiction of UN - Problem: No singulars in statements possible - All terms are universally quantifed - e.g., *Every Socrates is a philosopher* (Socrates is only a person) ###### Port-Royal-Logic - Arnauld/Nicole, 1662 - Idea: Introduce singulars as universal - e.g., *All Socrates are men.* - Looks awkward/weird ###### Criticism - 4th century BC: Eubulides of Miletus - e.g., *A grain of sand is no heap. Adding a single grain does not make a heap. => There is no heap of sand.* - Problem: - Natural language is not formal (not Aristotle's fault) - Term Logic uses unary predicates - 1879: Gottlob Frege - Responsible for the downfall of Term Logic - Recognized the need for *quantifiable variables* and *predicates* - Distinction between *object* and *concept* - *Morning Star is Venus* - *Venus is a planet* - Subject/object are not reversible => Different *is* - Results in predicate logic ##### Logicism - Based on Frege, 1879 - Task: - Axiomatize the new system of logic - View mathematics as an extension of logic - Build a mathematical logic for set theory - Foundation of analytic philosophy - Analyse philosophical propositions - Two trends: Neo-Positivism, Ideal language analysis - **1901: Russel's paradox**: - Frege's logic still contained contradictions - *Imagine a barber shaving all people iff they do not shave themselves. Does the barber shave himself?* - Russel constructs a set containing the sets which are not member of themselves - **Modern logical calculus**: - Book *Principia Mathematica* (by Russel and Whitehead) - Use axiomatic set theory - Idea: Find a complete and consistent set of axioms to derive every true theorem of the system - Results in the *Hilbert Program*: - David Hilbert axiomatized all mathematics - **Incompleteness theorem**: - Destruction by Kurt Gödel, 1931 - *Complete axiomatization* of all mathematics is not possible - *Incompleteness theorems* 1. If an axiomatic system is consistent, it can not be complete. 2. The consistency of axioms can not be proved in the axiomatic system itself. - **But**: - Gödel's completeness theorem: Completeness of first-order logics --- ### First-Order Logic #### Basics - Central idea: - Formally deduce from a set of facts - Which statements are *true* and which are *false* - Works due to the completeness theorem of FOL - Introduces the concept of *predicates* - *Predicate*: Property (group entities into types, e.g., man/student/strawberry) - Fine-grained quantification: Existential + Universal - Formalization: - Language: - Syntax - *How to valid sentences look like?* - Interpretation: - Semantics - *When is a statement true/false?* - System: - Mechanism called *Deduction* - *What statements can be deduced from a given set?* #### Syntax - FOL syntax mimics natural language - **Important**: Syntax has no meaning (without interpretation) - Concepts: - Formula (statement; basic building block) - Predicate (express sth. about a term) - Term (represent objects/concepts) - Constant - Variable (assign a value) - Function (apply on term) - Statement: - Contains a predicate (something is said about entity, e.g., `3 is even`) - Can be concatenated to a new statement using special connectives, e.g., *AND* - Has truth value - Quantification: - Variables can be quantified - *Universal quantification*: - Predicate must be valid for all valid substitutions of the variable - *Particular quantification*: - Predicate must be valid for at least one valid substitution of the variable - Language - Formal construction mechanism for statements ##### Signature - First-order logic language is quadruple (*signature*) - `$ \mathcal{L}=(\Gamma, \Omega, \Pi, X) $` - `$ \Gamma $`: - Non-empty finite set of constant symbols - e.g., a, b, Hector, 3, Frog - Constants may represent singular entities (but not types/collections) - `$ \Omega $`: - Set of functions - `$ \Omega = \bigcup_{n\in\mathbb{N}} \Omega_n $` - `$ \Pi $`: - Set of predicates - `$ \Pi = \bigcup_{n\in\mathbb{N}} \Pi_n $` - `$ \Pi_n $`: Set of n-ary predicates - e.g., `$ P, Q, R $` - Define sets of elements (constants evaluating predicates to *true* form a group) - Evaluate to either *true* or *false* - Substitution: - e.g., `$ P(x|_{x=Hector}) $` - `$ X $`: - Finite set of variables - e.g., `$ x,y,z $` - Variables may **only** be substituted by constant values - Higher-order logic: May substitute with predicates (increases complexity) - `$ \mathcal{L} $`: - *Signature* of the language - Signature is application-dependent - The *Universal signature* is commonly used - Contains all predicates and functions of all aritys ##### Term - *Constant*: - Represents objects or concepts - *Variable*: - Assign a value (objects/concept) - *Gain expressiveness using variables* - *Function*: - Can be applied on terms - e.g., `3+5 = +(3,5)` - *Term*: - *Yet un-interpreted expression* - Built from constants, variables and functions - Have no truth value, e.g., `2+6` - Definition `$ T_\mathcal{L} $`: - Constant symbols from `$ \Gamma $` are terms - Variables from `$ X $` are terms - Functions `$ f(t_1,\ldots,t_n) $` are terms iff `$ f\in\Omega_n $` and `$ t_1,\ldots,t_n $` are terms - *Ground term*: - Term without any variables ![](images/02-term.png) ##### Formula - Formulae are the basic building block (a *statement*) - Inserting terms into predicates are atomic formula - e.g., `even(2+6)` - *Yet un-interpreted statement* - Classification of formulae: - Atomic - Open/Closed - Rectified - Grounded - **Set of *atomic formulas* or *Atom***: - `$ A_\mathcal{L}=\{P(t_1,\ldots,t_n)\mid P\in\Pi_n, t_1,\ldots,t_n\in T_\mathcal{L}\} $` - State simple facts, defined by predicates - **Grounded formula**: - Formula without any variables - **Recursive definition**: - *Atomic formula* is a formula - If `$ W $` is formula, `$ \neg W $` is a formula - If `$ W_1 $` and `$ W_2 $` are formulas, the following are formulas: - `$ W_1 \land W_2 $` - `$ W_1 \lor W_2 $` - `$ W_1\Rightarrow W_2 $` - `$ W_1\iff W_2 $` - If `$ x $` is variable and `$ W $` is formula, `$ \forall x(W) $` and `$ \exists x(W) $` are formulas ![](images/02-formula.png) ##### Connectives - Apply on formulae (i.e., connect or modify) - Have certain hierarchy (to avoid parenthesis): 1. Quantifiers (`$ \forall, \exists $`) 2. NOT (`$ \neg $`) 3. AND (`$ \land $`) 4. OR (`$ \lor $`) 5. Implication and Equivalence (`$ \Rightarrow, \iff $`) ##### Variable Bindings - Formula `$ W $` has three sets of variables - *Free* variables `$ free(W) $` - *Bound* variables `$ bound(W) $` - All variables `$ vars(W)=free(W)\cup bound(W) $` - **Recursive definition**: - Formula `$ W $` is atomic: - `$ free(W)=vars(W) $` - `$ bound(W)=\emptyset $` - Negation `$ \neg W $`: - Negation has no effect - `$ free(\neg W)=free(W) $` - `$ bound(\neg W)=bound(W) $` - Binary connectives `$ \land,\lor,\Rightarrow,\iff $`: - Binary connectives merge sets - `$ free(W_1\land W_2)=free(W_1)\cup free(W_2) $` - `$ bound(W_1\land W_2)=bound(W_1)\cup bound(W_2) $` - Quantifiers `$ \forall ,\exists $`: - Quantifiers bind variables - `$ free(\forall x W)=free(W)\setminus \{x\} $` - `$ bound(\forall x W)=bound(W)\cup \{x\} $` - Classification of formula `$ W $`: - *Closed* iff `$ free(W)=\emptyset $` - Constant truth value - Depend on the interpretation - *Open* iff `$ free(W)\neq \emptyset $` - Truth value depends on free variables (*‌parameters*) - **Rectification**: - Bound variables are only valid *within their scope* - Variable can be free and bound at the same time (but independent) - Problem: Confusion - *Rectification*: Rename variables - `$ W $` is rectified iff `$ free(W) \cap bound(W) = \emptyset $` - **Closures**: - Closure operation: Quantify/bind all free variables - `$ free(W)=\{x_1,\ldots,x_n\} $` - Universal closure: `$ \forall x_1,\ldots,x_n(W) $` - Existential closure: `$ \exists x_1,\ldots,x_n(W) $` ![](images/02-syntax.png) #### Semantics - Assumption: - Formula is syntactically correct - Meaning of symbols is considered common sense (e.g., 5 means 5, `$ \land $` means AND) - Now: Interpretation of a language (and therefore statements) - Give meaning to the symbols of the syntax - Meaning of words/symbols? - Which values can variables have? - *Interpretation*: - Assigns an *element* of some Universe of Discourse to each *term* - Assigns truth value to each formula (*which statements are false/true*) - Capture the *semantics* of a language - *Universe of Discourse*: - Non-empty set of objects, entities and concepts - Contains entities/concepts related to our current application - e.g., subset of real world ##### Interpretation - *Interpretation of Language `$ \mathcal{L} $`* - `$ I_\mathcal{L}=(U, I_C, I_F, I_P) $` - `$ U $`: - Universe Of Discourse - All real objects, entities, concepts - These are not just symbols or names - `$ I_C $`: - `$ I_C: \Gamma\rightarrow U $` - Mapping of constants to the universe of discourse - e.g., `5` is the natural number 5 - `$ I_F $`: - Mapping of function symbols to real functions - `$ I_F(f_n): U^n\rightarrow U $` - e.g., `+` means addition - `$ I_P $`: - Mapping of predicate symbols to real predicates - `$ I_P(R)\subseteq U^n $` - e.g., `Frog(x)` means the type frog from the real world ##### Variable Substitution - `$ \rho: X\rightarrow U $` - Assign to each variable a value of the universe of discourse ##### Term Evaluation - Each term `$ t\in T_\mathcal{L} $` can be interpreted w.r.t. - (1) an interpretation `$ I_\mathcal{L} $` and - (2) a variable substitution `$ \rho $` - *Term evaluation* - `$ I^*_\rho(t) = t_I\in U $` - `$ t_I $` is the result of the interpretation of `$ t $` - Informal: - If term is a constant, use the constant interpretation - If term is a variable, look up the variable substitution - If term is a function, evaluate the function - Definition of `$ I^*_\rho(t) $`: - `$ t\in \Gamma \Rightarrow t_I=I_C(t) $` (constant) - `$ t\in X \Rightarrow t_I=\rho(t) $` (variable) - `$ t=f(t_1,\ldots,t_n)\Rightarrow t_I=I_F(f)(I^*_\rho(t_1),\ldots,I^*_\rho(t_n)) $` (function of terms) ##### Formula Evaluation - *Formula evaluation* `$ I_\rho: F_\mathcal{L} \rightarrow \{\text{true},\text{false}\} $` - Assumptions - *Closed World Assumption* - "Anything not mentioned in the universe of discourse does not exist" - Something not appearing in the predicate interpretation evaluates to *false* - *Open World Assumption*: - Assume UoD is incomplete - Formulas may be evaluate to *unknown* - Problem: Difficult for KBS because a system answering *unknown* is not very useful - Variable substitutions - Term evaluation does not assign truth values - Question: For which *substitutions* is a formula true? - Start of *Logic programming*, e.g., PROLOG ###### Atomic Formula - Atomic formula `$ W=S(t_1,\ldots,t_n) $` - `$ I_\rho(W)=\text{true}\iff I_\rho^*(t_1),\ldots,I_\rho^*(t_n)\in I_P(S) $` - Using *closed world assumption* ###### Non-atomic Formula - Use sub-formulas to evaluate concatenated formulas - Interpreting connectives: - Connective is a boolean, binary function (defined by truth tables) - `$ I_\neg, I_\land, I_\lor, I_\Rightarrow, I_\Leftrightarrow $` - Definition of `$ I_\rho:F_\mathcal{L} $` - `$ I_\rho(\neg W)=I_\neg(I_\rho(W)) $` - `$ \theta\in\{\land,\lor,\Rightarrow,\Leftrightarrow\}:I_\rho(W_1\,\theta\,W_2)=I_\theta(I_\rho(W_1),I_\rho(W_2)) $` ###### Quantified Formula - Requires *modified substitutions* - Goal: Modify values of a substitution - `$ I_{\rho(x|d)}, x\in X, d\in U $` - Substitute variable `$ x $` with element `$ d $`, the remaining variables are unchanged - Idea: - Formulae `$ \exists x(W) $` or `$ \forall x(W) $` - Un-bind variable `$ x $` and change its value using a modified substitution until the formula `$ W $` evaluate to either true or false - *Particular quantification*: - `$ \exists x(W) $` is **true** if there exists any element in the universe evaluating formula `$ W $` to true - `$ I_\rho(\exists x(W)) = \text{true iff }\text{true}\in\{I_{\rho(x|d)}(W) \mid d\in U\} $` - Using *closed world assumption* (otherwise statement can not be interpreted) - *Universal quantification*: - `$ \forall x(W) $` is **false** if there exists any element in the universe evaluating formula `$ W $` to false - `$ I_\rho(\forall x(W)) = \text{false iff }\text{false}\in\{I_{\rho(x|d)}(W) \mid d\in U\} $` - Using *closed world assumption* (otherwise statement can not be interpreted) #### Clauses - Definition *Literal*: - Set of literals `$ L_\mathcal{L} $` consists of all atomic formulae `$ A\in A_\mathcal{L} $` and `$ \neg $` - *Positive literal*: `$ A $` - *Negative literal*: `$ \neg A $` - *Ground literal*: No variable in literal - Definition *Clause*: - A clause is the Universal closure of a disjunction of literals - e.g., `$ \forall L_i\in L_\mathcal{L}:L_1\lor\ldots\lor L_n $` - Definition *Horn clause*: - A Horn clause is a clause with at most a single positive literal - e.g., `$ \forall (\neg L_1\lor\ldots\lor L_n) $` - Definition *Goal clause*: - Horn clause without a positive literal - e.g., `$ \neg A_1 \lor \neg A_2 $` - Definition *Definite clause*: - Horn clause exactly one positive literal - e.g., `$ \neg A_1 \lor A_2 $` - Definition *Fact clause*: - Horn clause with exactly one positive literal and no negative literals - e.g., `$ A $` - **Horn clause as implication** - `$ \neg A_1\lor A_2\equiv A_1\implies A_2 $` - A set of preconditions follows one fact (required for deductive databases) --- ### Models - Important question: Which *interpretation* and *variable substitution* make a formula true? - Problem: Unlimited possible interpretations and variable substitutions - Restriction: Use closed formulae - Variable substitution function irrelevant - Only rely on quantifiers - Definition *Model*: - Interpretation `$ I $` is a *model* **of** a closed formula `$ W $` iff `$ I_\rho(W)=I(W)=true $` - `$ I $` is model of a set of closed formulae `$ \mathcal{W} $` iff it is a model for every `$ W\in\mathcal{W} $` - Definition *Fact*: - Closed formula `$ W $` is a *fact* w.r.t. an interpretation `$ I $` if `$ I(W)=true $` #### Satisfiability - Question: Does a set of closed formulae `$ \mathcal{W} $` have a model? - Definition *Satisfiable* - `$ \mathcal{W} $` is called *satisfiable* iff `$ \mathcal{W} $` has a model - `$ \mathcal{W} $` is called *unsatisfiable* iff `$ \mathcal{W} $` does not have any model - Stop evaluation of an unsatisfiable set - Check for unsatisfiability is easier (really?) - Connection between *satisfiability of a set of formulae* and *inference*: - *To infer formulae, we must check for satisfiability* - Principle of indirect proof by Aristotle (*reductio ad absurdum*) - Goal: Prove `$ W $` using set of propositions `$ \mathcal{W} $` - Assume: `$ \neg W $` - Show contradiction to some statement in `$ \mathcal{W} $` - Thus, `$ \mathcal{W}\cup \{\neg W\} $` is unsatisfiable - `$ \mathcal{W}\models W \iff \mathcal{W}\cup \{\neg W\} \text{ is unsatisfiable} $` ![](images/04-classes.png) #### Semantic Equivalence - Question: Describe two concepts the same idea? (*redundant rules waste time/space*) - Definition: - `$ W_1 $` and `$ W_2 $` are semantically equivalent iff `$ \forall I: I(W_1)=I(W_2) $` - *Evaluation of both formulae is always the same* - *Can* be derived by using tautologies as transformation rules #### Semantic Conclusion - Question: Can a certain fact be deduced from a given set of facts? - Trade-off: - Query time vs. size of the IDB - i.e., store rule (so no conclusion must be drawn) or calculate rule at query time - Definition: - `$ W $` is semantic conclusion of `$ \mathcal{W} $` iff every model of `$ \mathcal{W} $` is also a model of `$ W $` - Notation: `$ \mathcal{W}\models W $` (`$ W $` follows from `$ \mathcal{W} $` #### Tautology - Class of formulae - *Every single interpretation is a model* - Definition *universal*: - `$ \mathcal{W} $` is *universal* if every interpretation is a model - Notation: `$ \models \mathcal{W} $` - Definition *Tautology* - `$ \mathcal{W} $` is a tautology if it is a *universal* - Use the set of all tautologies to derive semantic equivalences (tautologies as *transformation rules*) - Examples - `$ W\lor\neg W $` - `$ W_1\land W_2\implies W_1 $` - `$ W\equiv \neg\neg W $` #### Test for Unsatisfiability - Use Case: - When the user adds a formula, check if the formula is *semantically equivalent* or a *contradiction* - Redundancy: `$ \mathcal{W}\equiv W $` - Contradiction: `$ \mathcal{W}\cup \{W\} $` unsatisfiable - Lemma: - `$ \mathcal{W}\models \neg W \iff \mathcal{W}\cup \{W\} \text{ is unsatisfiable} $` - *Statement and contradiction can not be true at the same time* - The Test: 1. Test `$ \mathcal{W}\cup\{W\} $` is unsatisfiable 2. [Lemma]: Test `$ \mathcal{W}\models \neg W $` 3. [Definition]: Every model of `$ \mathcal{W} $` must be a model `$ \neg W $` 4. [**model-theoretical approach**]: Test all possible interpretations to find a model 5. [Problem]: Unlimited amount of interpretations (leads to Herbrand Theory) 6. [Herbrand Model]: Find a Herbrand Model of `$ \mathcal{W} $` (**only for clauses**) 7. [Herbrand Theorem]: Find a Herbrand Expansion not satisfying `$ \neg W $` (using Boolean Logic) - Problem: Unlimited amount of interpretations - Solution: - Use interpretations which are representative for the entire class of all interpretations (e.g., natural numbers, even numbers) - *Restrict to clauses and use Herbrand interpretations* - Problem: Approach is theoretical - This test for unsatisfiability can not be implemented - In deductive databases, the bottom-up approach is used - i.e., compute the transitive hull of `$ \mathcal{W} $` and test if the formula is satisfiable #### Herbrand Theory - **Goal**: - Define a representative interpretation which can replace any other (so-called *Herbrand Interpretation*) - Provide a reduction of first-order logic to propositional logic (only works for **clauses**) - Given a language `$ \mathcal{L} $` - *Herbrand interpretation* consists of two parts: - *Herbrand Universe* `$ U_\mathcal{L} $` - Consists of all ground terms - Only use constants and functions, no variables - *Herbrand Base* `$ B_\mathcal{L} $` - Contains all ground atoms, i.e., no variables - *‌Take all the terms of the Herbrand universe and apply the predicates of the language `$ \mathcal{L} $` to them* - Infinite set - `$ P(t_1,\ldots,t_n)\subseteq B_\mathcal{L} $` with `$ t_i\in U_\mathcal{L} $` ##### Herbrand Interpretation - Definition - `$ I=(U,I_C,I_F,I_P) $` - `$ U=U_\mathcal{L} $` (Herbrand Universe) - `$ I_C(c)=c $` (interprete by itself) - `$ I_F(f):U_\mathcal{L}^n\rightarrow U_\mathcal{L}, f(t_1,\ldots,t_n)\mapsto f(t_1,\ldots,t_n) $` (interprete by itself) - **‌Completely symbolic/syntactical interpretation without a specific real-world semantics** - Term `$ f(x) $` has no meaning (just a symbol) - Universe element `$ f(x) $` is interpreted (meaning) - Difference between multiple Herbrand Interpretations: - `$ U, I_C, I_F $` are always the same - Only difference: - Predicate Interpretation `$ I_P $` - Idea: - Define a Herbrand interpretation only by *listing* the atoms which evaluate to true and all others are false - Interpretation is defined by the subset of the Herbrand Base `$ I\subseteq B_\mathcal{L} $` - Results in *Closed World Assumption* (everything not mentioned is false) ##### Herbrand Model - Definition - A *Herbrand model* of a set of formulae `$ \mathcal{W} $` is a Herbrand interpretation which is a model `$ \mathcal{W} $` - Example: - Formula: `$ W\equiv\forall x,y(loves(x,y)\implies loves(y,x)) $` - `$ I_1=\{loves(Tarzan, Jane), loves(Jane, Tarzan)\} $` is a Herbrand Model - `$ I_2=\{loves(Tarzan, Jane), loves(Jane, Paul)\} $` is **not** a Herbrand Model - Lemma: - Given set of **clauses** `$ \mathcal{W} $` - `$ \mathcal{W} $` has model *if and only if* `$ \mathcal{W} $` has a Herbrand model - `$ \mathcal{W} $` is unsatisfiable if and only if `$ \mathcal{W} $` has no Herbrand model - Meaning: *Syntactical interpretation of all symbols* - Idea: - If some syntactical interpretation can satisfy the set of clauses, there is some semantic interpretation (more or less useful) - Test for Unsatisfiability: - *see above* - Instead of testing all models of `$ \mathcal{W} $`, only show the (non-)existance of a single Herbrand model - *Only works for clauses not for general closed formulas* --- ### Complexity (D) - Use Case: - Deductive DB checks if a *given statement* can be *deduced* from a given set of formulae - Check `$ \mathcal{W}\models W $` (`$ \mathcal{W}\cup\{W\} $`) - Focus: Computational complexity (for databases this is important) - Check for validity (tautology) - Check for satisfiability - Sets of expressions: - *VALID* (tautology) - `$ \models W $` - *SATISFIABLE* (but not valid) - *UNSATISFIABLE* - Negation as *mirror operation* - *Check for classes*: - Satisfiable: Generate substitution, evaluate - `$ W $` valid: Check if `$ \neg W $` is unsatisfiable - `$ W $` unsatisfiable: Check if `$ W $` is satisfiable - Satisfiability: - Propositional logic: Decidable - First-order logic: Undecidable ![](images/04-3-classes.png) #### Propositional Logic - SAT problem: - *‌Satisfiability problem* - Is a given propositional formula satisfiable? - Complexity class: NP-C ##### SAT Algorithms - **Deterministic decidable algorithm** - Generate all `$ 2^n $` substitutions - Evaluate all substitutions (`$ O(n^2) $` per substitution) - Overall `$ O(n^2 2^n) $` - **Non-deterministic semi-decidable algorithm** - Guess any substitution - Evaluate this substitution (`$ O(n^2) $`) - Continue until the evaluation is `$ true $` - **Construct a substitution** - Idea: Construct a substitution using the formula - e.g., *one variable must be true and one has to be false* - i.e., *exclude certain substitutions* - Problem: Hard for general formulae - **Davis-Putnam Algorithm** - Default algorithm to solve SAT - Formula must be in *conjunctive normal form* - `$ O(1.8^n) $` - Idea: Build a pruned tree of possible substitutions ##### SAT Variants - **3-SAT** - Formula must be conjunctive normal form where each clause contains at most 3 literals - First problem shown to be *NP-complete* - SAT reduces polynomially to 3-SAT - **Horn-SAT** - SAT with conjunctive normal form where each clause is a Horn clause - *Important*: *P-complete* - Idea: - Write Horn clause in implication form - Facts: `$ true\rightarrow x_1 $` - Definites: `$ x_1\rightarrow x_2 $` - Goals: `$ x_1\land x_2\rightarrow false $` - A set of Horn clauses is satisfiable iff all conjunctions of implications is true - Find variables which have to be true - Algorithm: 1. Set `$ T=\emptyset $` contains all variables which must be *true* (all others are *false*) 2. Pick any (currently) unsatisfied/false implication - `$ H_i\equiv\bigwedge x_j\Rightarrow y $` - Must be a *fact* or a *definite* 3. Add `$ y $` to `$ T $`: `$ T=T\cup \{y\} $` 4. Repeat, until no unsatisfied/false implications exist 5. Result: Iff `$ T $` satisfies all clauses, `$ \mathcal{W} $` is satisfiable #### First-Order Logic - Problem: - Universe of potentially unlimited size (interpretations) - Quantifiers (formula must be true for subset of universe) ##### Example (Number Theory) - Language - `$ \mathcal{L}_{NT}=(\{0\}, \{\sigma, +,\times, \uparrow\}, \{=,<\},\{x,y,z\}) $` - Interpretation - Universe: All natural numbers - Successor function `$ \sigma $`: - `$ \sigma(\sigma(\sigma(0)))=3 $` - Shortcut: Decimal numbers - Functions and functions are interpreted common sense - Naive evaluation: Testing all values is very problematic - e.g., `$ \exists x(x>2000) $` - Problem: - Testing for all possible substitutions in an infinite universe does not work ##### Peano Arithmetic - Guiseppe Peano, 1889 - Idea: - Use deductive system to construct a proof (from a set of valid axioms) - Do **not** test all possible values - Axiomatization of Number Theory - 15 axiom types inducing countable unlimited number of axioms ##### Fermats Last Theorem - `$ \neg\exists n,a,b,c((a^n+b^n=c^n\land n>2) $` - Took very long (357 years) to show that this statement is provable for the natural numbers - 1995: Proved by Andrew Wiles ##### Gödel's Incompleteness Theorem - *[...] generated theory can not be both consistent and complete. [...]* - e.g., some statements are provable in the Peano arithmetic (Goodstein Theorem and Fermats Last Theorem) - Result: - For any non-trivial deductive system `$ NT $`, there exists a statement, which can not be proved within this system - *Unprovable* is called *undecidable* - `$ NT\vdash W $`: `$ W $` can be proved in system `$ NT $` - Note: - First-order logic can not be used to model infinite domains (e.g., the natural numbers) - Hence, the incompleteness theorem does not apply to FOL ![](images/04-classes.png) ##### Goodstein Theorem - Statement about the natural numbers (*Hercules fighting the Hydra*) - *Goodstein sequence eventually terminates at 0* - `$ Goodstein(3)=3,3,3,2,1,0 $` - `$ Goodstein(4)=4,26,41,\ldots,299,\ldots,0 $` - Theorem is expressible and true in the Peano arithmetic ##### Paris-Kirby Theorem - *Goodstein Theorem is not decidable* - Can not be proven in Peano Arithmetic (or First-Order Logic) - Why? - Consistency of Peano arithmetic would follow from the proof of the Goodstein Theorem - This is not possible due to Gödel's incompleteness Theorem (Peano arithmetic can not prove its consistency) ##### Herbrand Theorem - Jacques Herbrand, 1928 - Informal: - **Closed** formula `$ A $` in **universal prenex form** is unsatisfiable iff there is a **finite** subset of the Herbrand expansion of `$ A $` `$ TA\subseteq E(A) $` which is Boolean unsatisfiable - **Result**: - Transform the First-Order Logic satisfiability problem to the Propositional Logic Satisfiability Problem (using this restriction) - By assigning a truth value to each predicate in a ground instance the formula represents a propositional logic formula ##### Formalization - *Universal prenex form*: - Prefix: Universal Quantifier binding all variables - Matrix: Formula without quantifiers - `$ \forall y_1,\ldots,y_n (F(y_1,\ldots,y_n)) $` - `$ F $` is quantifier-free - *Instance of `$ A $`*: - Formula where variables of `$ A $` are substituted by entities - *‌Herbrand expansion `$ E(A) $`*: - Set of all possible ground instances of `$ A $` with all substitutions from the Herbrand base - *Herbrand Theorem*: - `$ A\equiv\forall y_1,\ldots,y_n(F(y_1,\ldots,y_n)) $` - `$ A $` is unsatisfiable if and only if there is a finite set `$ TA\subseteq E(A) $` of ground instances such that `$ TA $` is unsatisfiable - Considerations: - Check of `$ TA $` can be performed in finite time - e.g., Davis-Putnam algorithm - Problem: Which `$ TA\subseteq E(A) $` is unsatisfiable? - Reducing to the *Halting problem* ###### Gilmore Algorithm - 1960 - Meta-algorithm to check for unsatisfiability - Algorithm: - Input: - FOL formula `$ A $` - Transform to universal prenex form (i.e., pull quantifiers and convert to universal quantifier) - Criterion: - Herbrand Expansion must be *generateable* (i.e., recursively enumerable) - i.e., `$ E(A)=\{A_1,A_2,\ldots\} $` - `$ k:=1 $` - `WHILE ` `$ \bigwedge_{i=1}^k A_i $` ` is satisfiable: k++` (*while not unsatisfiable*) - `RETURN 'A unsatisfiable'` - Semi-decidable algorithm (only terminates if `$ A $` is unsatisfiable) ###### Schönfinkel-Bernays Class - **Restriction**: Allow only a decidable subset of formulae - *Schönfinkel-Bernays class* - No functional symbols - No equality predicate - Formula `$ W $` in prenex form - SB-SAT: - Satisfiability of formulae of SB-class is *decidable* - Proof: - No functional symbols - --> Finite Herbrand Base - --> Finite Herbrand Expansion - --> Generation in finite time - --> Finite time for the unsatisfiability check - Problem: - SB-SAT is in NEXP-C - NEXP: Non-deterministic exponential time algorithm - No functional symbols (restricts expressiveness) ###### Restriction - *Do we need full First-Order Logics?* - Requirements: - Subset of FOL with guaranteed finite Herbrand expansions - Better complexity than NEXP - Subset should not limit expressiveness - Restriction: - Restrict to **Horn clauses** - Finite Herbrand universe - Check is in P - Restrict to **Non-recursive typed functions** - Advantage: - Check for unsatisfiability of finite subsets of Herbrand expansion is in `$ PTIME $` --- ### Deductive Systems (D) - Question: How to find the set of all tautologies? - *Find the universal truth* - Automatically proof theorems - Approaches: - Model-theoretical (this course) - Bottom-up approach (find a Herbrand model) - Proof-theoretical - Hilbert-Style deduction system - Natural deduction - David Hilbert - Mathematician in Göttingen (also university of Gauss and Riemann) - Königsberg, 1862 - Pioneer in proof theory and logics - The Hilbert Program - Started in 1920 - Goal: Completely formalize math to finite, complete set and axioms - Preciseness: Use precisely defined formalisms - Completeness: All math can be proved by a system - Consistency: No contradictions will show up - Decidability: For each statement, an algorithm can decide if it is true - *Gödel incompleteness theorem*: - Prove that the Hilbert Program is impossible #### Deduction Theorem - `$ \mathcal{W}\cup\{W_1\}\models W_2\iff \mathcal{W}\models W_1\implies W_2 $` - *Fundamental Meta-Rule*: Deduction theorem is considered true in every system but not a theorem of that system - Inference rules: - Modus Ponens (Implication Elimination Rule) - Abduction Inference Rule ##### Modus Ponens - *‌Implication Elimination Rule* - `$ \{W_1, W_1\implies W_2\}\models W_2 $` - *Sound*, i.e., never generates incorrect knowledge - Example (for not-sound): - Fact `$ W_1 $`: Today is Tuesday - Rule `$ W_1\implies W_2 $`: If today is Tuesday, today is KBS lecture - Derived `$ W_2 $`: Today is KBS lecture - *Usually sufficient for axiomatic systems* ##### Abduction Inference Rule - `$ \{W_1\implies W_2, W_2\}\models W_1 $` - *Not sound* - Often helpful, used in medicine - Example: - Rule `$ W_1\implies W_2 $`: If it rains, it is wet - Fact `$ W_2 $`: It is wet - Derived `$ W_1 $`: It has rained #### Hilbert-Style Deduction System - *Deduction System*: Logic - Also called *Axiomatic systems* - Hilbert-style deduction system for a language `$ \mathcal{L} $` - Components: - *Logical axioms* - Set of formulae of `$ \mathcal{L} $` - Can not be proven that they are true/false - *Inference rules* - Set of rules to transform one statement to another - Deduction System generates proofs - Axiom must be an instance of the following schemes: - A1: `$ A\Rightarrow(B\Rightarrow A) $` - A2: `$ (A\Rightarrow (B\Rightarrow C))\Rightarrow((A\Rightarrow B)\Rightarrow(A\Rightarrow C)) $` - A3: `$ (\neg A\Rightarrow\neg B)\Rightarrow(B\Rightarrow A) $` - All axioms are *tautologies* - There is an *unlimited* number of axioms - *Proof from `$ \mathcal{W} $` to `$ A $`*: - Finite sequence `$ W_1,\ldots,W_n $` of formulae of `$ \mathcal{L} $` such that `$ W_i $` is either an axiom or follows from one of the previous `$ W_j $` by the inference rules - Example: - Prove: `$ \models \neg B\Rightarrow (B\Rightarrow A) $` 1. `$ \neg B\models B\Rightarrow A $` (Deduction theorem) 2. `$ \neg B $` (Hypothesis) 3. `$ \neg B\Rightarrow (\neg A\Rightarrow\neg B) $` (Axiom 1) 4. `$ \neg A\Rightarrow\neg B $` (Modus Ponens) 5. `$ (\neg A\Rightarrow\neg B)\rightarrow(B\Rightarrow A) $` (Axiom 3) 6. `$ B\rightarrow A $` (Modus Ponens) - Drawbacks: - Few rules but many axioms (contradicts goals of deductive databases) - Finding proofs is tricky (trial and error) - Feels unnatural #### Natural Deduction - Gerhard Gentzen, 1938 - Use more rules but a limited set of axioms - Later been adapted to deductive databases - Concepts: - Axioms (tautologies) - Logical rules - Structural rules (syntactical)