SC Chapter 4 First Order Logic
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 4 First Order Logic
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 4 First Order Logic
-
- 1 / 25
-
Cartes-fiches
What are the non-logical symbols of FO? [5]
1. Non-logical symbols can differ
2. Constants C // 0 1
3. Variables V // x y
4. Function symbols F // binary +
5. Predicate symbols P // binary > =, from theory to logical
What is a free or bounded variable in FO?
Free if variable is not specified in quantifier else bound
What theory expressions exist in FO? [2]
1. Terms and 2. constraints
What is the definition of terms in FO? [2]
1. All c and v
2. All f(t1,…,tn) with t1,…,tn terms and n>0
What is the definition of constraints in FO?
All P(t1,…,tn) with t1,…,tn terms
What is the definition of a signature Sigma?
Restrict non-logical symbols to a set // Sigma = {0,1,+,=}
What is the definition of a Sigma-formula?
Formula with symbols from Sigma
What is the definition of a Sigma-sentence?
Sentence a Sigma-formula without free variables
What is the definition of a Sigma-structure?
Domain D Interpretation I and assignment alpha
What is the definition of an interpretation I? [4]
1. Restrict non-logical symbols
2. C → D
3. F → (D^n → D)
4. P → (D^n → {true, false})
What is the definition of an assignment alpha?
free(V) → D
What can be deduced from an assignment alpha? [2]
1. alpha of phi is word
2. All alpha (words) of phi is language
What holds for two languages L1 and L2? [3]
1. L1 < L2 defines L2 is more expressive
2. L1 and L2 have same complexity → reducible
3. L1 and L2 reducible → same complexity depends on reduction complexity
What holds for more expressive languages?
More expressive language can be even undecidable
What is the definition of satisfiability of a structure S and formula phi? [4]
1. S is model of phi
2. S,alpha |= phi with phi a Sigma-formula
3. S |= phi with phi a Sigma-sentence
4. Valid if for all S,alpha
What is the definition of a theory T? [4]
1. Restrict interpretation
2. Set Se of Sigma-sentences
3. Large to infinity
4. Alternative is set of axioms A
What is the definition of T-satisfiability? [2]
1. phi if S,alpha |= phi and S |= Se
2. Valid if for all S |= Se
What are examples for theories? [6]
1. Presburger arithmetic // 0,1,+,> with Z
2. Peano arithmetic // 0,1,+,*,> with Z
3. Linear real arithmetic // 0,1,+,> with R
4. Real arithmetic // 0,1,+,*,> with R
5. Theory of arrays
6. Theory of pointers
What are the logical symbols of FO? [3]
1. Logical symbols are fix
2. Connectives // unary \neg and binary \land …
3. Quantifiers // \forall \exist
What is the definition of wff in FO? [3]
1. All constraints are atomic formulas (af)
2. Connectives applied on wff are wff
3. Quantifiers applied on wff are wff
What is the order of operators for omitting parentheses in FO?
-- || \forall \exist ↔ → \or \and \neg || ++
What are the semantic rules in FO? [7]
1. Constants [c]_S,alpha = I(c)
2. Variables [v]_S,alpha = alpha(v)
3. Functions [f(t1,…,tn)]_S,alpha = I(f)([t1]_S,alpha,…,[tn]_S,alpha)
4. Predicates S,alpha |= p(t1,…,tn) iff I(p)([t1]_S,alpha,…,[tn]_S,alpha)
5. Negation S,alpha |= \neg phi iff S,alpha !|= phi
6. And S,alpha |= phi \land psi iff S,alpha |= phi AND S,alpha |= psi
7. Exist S,alpha |= \exist x (phi) iff v \in D with S,sigma(x→v) |= phi
What are the characteristics of logic fragments? [4]
1. Restrict grammar and logical symbols
2. Abstract grammar and no restriction and fixed interpretation of symbols
3. Resolution is sound and complete for propositional logic but not for higher theories (Peano undecidable and Presburger decidable)
4. Decidable theories can be tractable (polynomial) or intractable (exponential)
What are the characteristics for the logic fragment propositional logic? [2]
1. Quantifier-free // With quantifiers we obtain quantified boolean formulas (QBF)
2. Signature with variables x1,…,xn and predicate identity and no axioms
What are the advantages of logic fragments? [3]
1. Expressible enough // More natural expressible some models
2. Decidable (semi-)
3. More efficiently solvable than richer theories
