Logic for Computer Science / Logica voor computertechnolgie. Samenvatting van de gegeven notites van de docent hoofdstuk 1 & deel hoofdstuk 2. Deze stof wordt naast het boek Modelling Computing Systems getoetst voor het examen. Gegeven op Universiteit Utrecht.
Given a formula in propositional logic p, we can check when p holds for all possible values of its
atomic propositional variables that occur in that formula whether the formule holds under a certain
assignment of false and true– this is what we do when we write a truth table.
We can also give a ‘proof sketch’ using proof strategies – but we haven’t made precise what these
strategies are, relying on an informal diagrammatic description. Can we define a set of all proofs of
some propositional logic formula? After all, we managed to define the syntax of propositional logic
as inductively defined set – can we do the same for its semantics?
We can define the syntax of propositional logic using BNF, we have different way to build a
propositional formula as follows:
p, q ::= true | false | P | ¬p | p ∧ q | p ∨ q | p ⇒ q | p ⇔ q
So far, we have seen the BNF notation for inductively defined sets. But what notation should we use
for inductively defined relations? For example, we defined the ⩽ relation between Peano natural
numbers using the following rules:
− for all n ∈ N, 0 ⩽ n;
− if n ⩽ m, then s(n) ⩽ s(m)
Inductively defined relations are often given by means of inference rules:
Here we have two inference rules, named Base and Step; these rules together
define a relation (⩽) ⊆ N × N. The statements above the horizontal line are the
premises - the assumptions that you must establish in order to use this rule; the
statement under the horizontal line is the conclusion that you can draw from
these assumptions.
These rules state that there are two ways to prove that n ⩽ m:
− if n = 0 the ⩽-Base rule tells us that 0 ⩽ n – for any n;
− if we can show n ⩽ m, we can use the ⩽-Step rule to prove s(n) ⩽ s(m).
A rule without premises is called an axiom.
Example:
By repeatedly applying these rules, we can write larger proofs.
For example, to give a formal proof that 2 ⩽ 5 we write:
We can read these rules top-to-bottom or bottom-to-top. Such a
proof is sometimes referred to a as derivation. Each of the
inference rules gives a different ‘lego piece’ that we can use to
write bigger proofs.
, Example of even numbers: We can use this inference rule notation to write all
kinds of relations. For example, we may want to define the unary relation
isEven – that proves that a given number is even.
Example of isSorted array: Similarly, we can define inference rules that
make precise when a list of numbers is sorted. Note that we can require
more than one hypothesis – as in the isSorted-Step rule.
A word over an alphabet Σ is called a palindrome if it reads the
same backward as forward. Examples include: ‘racecar’, ‘radar’, or
‘madam’. Give a inference rules that characterise a unary relation
on words, capturing the fact that they are a palindrome.
Hoofdstuk 2 Natural Deduction
Given the following set of propositional logical formulas over a set of atomic variables P: p, q ::= true
| false | P | ¬p | p ∧ q | p ∨ q | p ⇒ q | p ⇔ q Can we give inference rules that capture precisely the
tautologies? Yes! These inference rules, sometimes called natural deduction, formalize the proof
strategies that we have seen previously.
Conjunction introduction and elimination
Conjunction introduction:
The proof strategy for conjunction introduction
and the inference rule for conjunction
introduction.
Voordelen van het kopen van samenvattingen bij Stuvia op een rij:
Verzekerd van kwaliteit door reviews
Stuvia-klanten hebben meer dan 700.000 samenvattingen beoordeeld. Zo weet je zeker dat je de beste documenten koopt!
Snel en makkelijk kopen
Je betaalt supersnel en eenmalig met iDeal, creditcard of Stuvia-tegoed voor de samenvatting. Zonder lidmaatschap.
Focus op de essentie
Samenvattingen worden geschreven voor en door anderen. Daarom zijn de samenvattingen altijd betrouwbaar en actueel. Zo kom je snel tot de kern!
Veelgestelde vragen
Wat krijg ik als ik dit document koop?
Je krijgt een PDF, die direct beschikbaar is na je aankoop. Het gekochte document is altijd, overal en oneindig toegankelijk via je profiel.
Tevredenheidsgarantie: hoe werkt dat?
Onze tevredenheidsgarantie zorgt ervoor dat je altijd een studiedocument vindt dat goed bij je past. Je vult een formulier in en onze klantenservice regelt de rest.
Van wie koop ik deze samenvatting?
Stuvia is een marktplaats, je koop dit document dus niet van ons, maar van verkoper luukvaa. Stuvia faciliteert de betaling aan de verkoper.
Zit ik meteen vast aan een abonnement?
Nee, je koopt alleen deze samenvatting voor €2,99. Je zit daarna nergens aan vast.
