- Simple(proposition constants) - express single facts about the world
- Compound - express logical relationsheeps among simpler sentences of which composed
- Negation - target
- Conjuction - tha argument of conjuction are called conjucts
- Disjunction - disjuncts
- Implication (p=>q) - p: antecedent(ենթադրյալ), q:consequent (հետևանք)
- Reduction (q <= p) - q: consequent, p: antecedent
- Equivalence / Biconditional (p <=> q)
- Precendence of connectives (նախորդում, ավելի բարձր դիրք, приоритет)
~
&
v
>, <, <=>
is the set of all propositional sentences that can be formed from propositional vocabulary.
- Proposition vocabulary is a set/sequence of proposition constants.
- Replace proposition constants by their truth values.
- Use operator semantics to simplify compound sentences with truth values as arguments.
- Repeat this inside-out fashion to produce a value for the sentence as a whole.
- Double Negation: p <=> ~~p
- deMorgan’s Laws: ~(p&q) <=> (~p v ~q) ~(p&q) <=> (~p & ~q)
- Implication Introduction: p => (q => p)
- Implication Distribution: (p => (q => r)) => ((p => q) => (p => r))
| p | q | p | (p v q) | |
|---|---|---|---|---|
| 1 | 1 | 1 | 1 | + |
| 1 | 0 | 1 | 1 | + |
| 0 | 1 | 0 | 1 | |
| 0 | 0 | 0 | 0 |
{p,q} entails (p & q) p,q, premises (p & q) logical conclusion from promosies p and q
| p | q | p | q | (p & q) | |
|---|---|---|---|---|---|
| 1 | 1 | 1 | 1 | 1 | + |
| 1 | 0 | 1 | 0 | 0 | |
| 0 | 1 | 0 | 1 | 0 | |
| 0 | 0 | 0 | 0 | 0 |
| left | from stanford | Question | Response | |
|---|---|---|---|---|
| 1 | 1 | 1 | 1 | + |
| 1 | 0 | 0 | 1 | |
| 0 | 1 | 0 | 0 | |
| 0 | 0 | 1 | 0 |
Question: Is it the case that the left road the way to the stadium if and only if you are from Stanford?
▶SAT: determines wheather a set of propositional sentences is satisfiable. Logic problems react as SAT problems (e.g entailment) SAT solvers used in
- Haedware design
- Software analysis
- Planning
- Mathematics
▶Methods used in SAT
- Complete methods
Guraranteed to give correct answer Truth Tables Backtracking search (Поиск с возвратом)
- Incomplete methods
Not guraranteed to give correct answer Local Search
▶Example Let Ψ = {p v q, p v ~q, ~p v q, ~p v ~q v ~r, ~p v r} Q: is Ψ satisfiable? Thas there is exsit a truth assignment that satisfied every sentence in Ψ? Assume each sentence in Ψ is a disjunction of atmos or negated atoms Solution: • Truth Table method - Complete method
| p | q | r | p v q | p v ~q | ~p v q | ~p v ~q v ~r | ~p v r | Ψ sat. |
|---|---|---|---|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 1 | 1 | 1 | 0 | no |
| 0 | 0 | 1 | 0 | 1 | 1 | 1 | 1 | no |
| 0 | 1 | 0 | 1 | 0 | 1 | 1 | 1 | no |
| 0 | 1 | 1 | 1 | 0 | 1 | 1 | 1 | no |
| 1 | 0 | 0 | 1 | 1 | 0 | 1 | 0 | no |
| 1 | 0 | 1 | 1 | 1 | 0 | 1 | 1 | no |
| 1 | 1 | 0 | 1 | 1 | 1 | 1 | 0 | no |
| 1 | 1 | 1 | 1 | 1 | 1 | 0 | 1 | no |
Complete: thruth table method is complete, because we examine every single truth assignment Impractical except for small examples rows
- 2 ^ 3 = 8
- 2 ^ 10 = 1024
- 2 ^ 20 = 1 million (10 ^ 6)
- 2 ^ 30 = 1 billion (10 ^ 9)
- 2 ^ 40 = 1 trillion(10 ^ 12)
• Partial assignments
| p | q | r | p v q | p v ~q | ~p v q | ~p v ~q v ~r | ~p v r | Ψ sat. |
|---|---|---|---|---|---|---|---|---|
| 1 | 0 | ? | 1 | 1 | 0 | 1 | ? | no |
| 1 | 0 | ? | 1 | 1 | 0 | 1 | ? | no |
because we have already the False in row and we do not need to check other sentences, we already no that answer is no.
• Searching partial assignments instead of only complete assignments. Tree like ??? / \ p false p true 0?? / this idea base rise to the basic backtracking search
▶ Basic backtracking search Essential backtracking search optiomization
- Unit propagation
- Pure Literal elimination
Most modern complete SAT sovlers are based on variations of DPLL (Davis-Putman-Logemann-Loveland)
- Clause Learning
- Fast Propagation
- Proposition selection heuristicc
➤ incomplete method Some SAT problems still impractical for complete SAT sovlers Little opportunity for early pruning (Էտում) Consider method that answer correctly most of the time, but not every time
GSAT: a prototype incomplete SAT solver WalkSAT: a modification of GSAT
Excerise exercise Video inline quize Пра́вило резолю́ций — это правило вывода, восходящее к методу доказательства теорем через поиск противоречий; используется в логике высказываний и логике предикатов первого порядка. Правило резолюций, применяемое последовательно для списка резольвент, позволяет ответить на вопрос, существует ли в исходном множестве логических выражений противоречие.Правило резолюций предложено в 1930 году в докторской диссертации Жака Эрбрана для доказательства теорем в формальных системах первого порядка. Правило разработано Джоном Аланом Робинсоном в 1965 году.Ex 1. Ex 2. Clausal Form Premises: {p, p => q, (p => q) => (q => r)} Conlclusion: r
| Premises: | Clauses: |
|---|---|
| p | {p} |
| p => q | {~p,q} |
| (p=>q)=>(q=>r) | {~p,~q,r} |
| {~q,r} | |
| ~r | {~r} |
Resolution proof:
| 1 | {p} | Premise |
| 2 | {~p,q} | Premise |
| 3 | {~p,~q,r} | Premise |
| 4 | {~q,r} | Premise |
| 5 | {~r} | Premise |
| 6 | {q} | 1,2 |
| 7 | {r} | 4,6 |
| 8 | {} | 5,7 |
|---|
⊃, ∨, ∧, ¬, ≡, ≠, ∀, ∃, λ, ≤, ≥, ∈, ∉, ∞,
When we want to say things more generally, we find that Propositional Logic is inadequate. Suppose, for example, that we wanted to say that, in general, if one person knows a second person, then the second person knows the first.▶Relational Logic is an extension of Propositional Logic that solves this problem. The trick is to augment(ավելացնել) our language with two new linguistic features, viz.
- variables
- quantifiers
With these new features, we can express information about multiple objects without enumerating those objects; and we can express the existence of objects that satisfy specified conditions without saying which objects they are.
▶We will proceed through the same stages as we did for Propositional Logic.
- syntax and semantics of our language.
- properties of relational logic sentences
- evaluation and satisfaction
- logical entailment.
- proofs (as with Propositional Logic, we leave the discussion of proofs to later chapters)
- Variables u,w,x,y,z
- Constants
a, b, c, 123, comp125
Types
- Object constants represent objects. e.g. joe, stanford, usa
- Function constatns replresent functions. e.g. father, mother, age, plus, times
- Relation constants represent relations. e.g. knows, loves
- Arity
the number of arguments a function constant or a relation constant it takes.
- Unary - function or relation constant - 1 argument
- Binary - function or relation constant - 2 argument
- Ternary - function or relation constant - 3 argument
- n-ary - function or relation constant - n argument
- Vocabulary(signature) of our language
consists of a set of object constants, a set of function constants, a set of relation constants, and an assignment of arities for each of the function constants and relation constants in the vocabulary. ▶ Terms - these words can be combined to form complex expressions called terms
- A term is either a variable, an object constant, or a functional term Terms represent objects. Terms are analogues to noun phrases in natural language.
- A functional expression, or functional term is an expression formed from n-ary function constant and n terms enclosed in parenthesis and spearated by commas. g(a,a) g(a,y) g(y,y) Funnctional terms are terms so can be nested g(g(a,y), g(y,a))
▶ Sentences How terms can be combined to form sentences Three type of sentences in relational logic. ▶ Relational sentences - analogues to the simple sentences in natural language or the analog of propositions in Propositional Logic is an expression formed from n-ary relation constant and n terms enclosed in parenthesis and spearated by commas. q(a,y) Relational sentences are not terms and cannot be nested in terms or relational sentences ▶ Logical sentences - analogous to the logical sentences in natural language or analogous to the logical sentences in Propositional Logic Logical sentences in Relational logic are analogus to those in Propositional logic. (~q(a,b)) (p(a) ∧ p(b)) (p(a) ∨ p(b)) (q(x,y) ⊃ q(y,x)) (q(x,y) ≡ q(y,x))
▶ Quantified sentences - sentences that express the significance(կարեւորություն) of variables(which have no analog in Propositional Logic)
- Universally quantified sentences - assert fact about all objects. (∀) Universal sentences used to assert that all object have a certain property (∀x.p(x) ⊃ q(x,x))
- Exsistentially quantified sentences - assert the existence of objects with given properties.(∃) Existential sentences used to assert that there are object have a certain property (∃x.(p(x) ∧ q(x,x)))
- Note that quantified sentences can be nested within other sentences (∀x.p(x)) ∨ (∃x.q(x,x)) (∀x.(∃x.q(x,y)))
- The quantifiers have higher precedence than logical operations ∀x.p(x) ⊃ q(x,x)
▶ Ground and Non-Ground expressions
- Ground An expression is ground iff it contains no variables. p(a)
- Non-Ground ∀x.p(x)
▶ Bound and Free Variables An occurence of variable is bound iff it lies in the scope of a quantifier of that variable. Otherwise it is free. ∃y.q(x,y) - in this example, x is free and y is bound.