Summary Modelling Computing Systems Extra notities H1 / H2 Faron Moller & Georg Struth
14 vues 0 achat
Cours
Logic For Computer Science (INFOB1LI)
Établissement
Universiteit Utrecht (UU)
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.
Les avantages d'acheter des résumés chez Stuvia:
Qualité garantie par les avis des clients
Les clients de Stuvia ont évalués plus de 700 000 résumés. C'est comme ça que vous savez que vous achetez les meilleurs documents.
L’achat facile et rapide
Vous pouvez payer rapidement avec iDeal, carte de crédit ou Stuvia-crédit pour les résumés. Il n'y a pas d'adhésion nécessaire.
Focus sur l’essentiel
Vos camarades écrivent eux-mêmes les notes d’étude, c’est pourquoi les documents sont toujours fiables et à jour. Cela garantit que vous arrivez rapidement au coeur du matériel.
Foire aux questions
Qu'est-ce que j'obtiens en achetant ce document ?
Vous obtenez un PDF, disponible immédiatement après votre achat. Le document acheté est accessible à tout moment, n'importe où et indéfiniment via votre profil.
Garantie de remboursement : comment ça marche ?
Notre garantie de satisfaction garantit que vous trouverez toujours un document d'étude qui vous convient. Vous remplissez un formulaire et notre équipe du service client s'occupe du reste.
Auprès de qui est-ce que j'achète ce résumé ?
Stuvia est une place de marché. Alors, vous n'achetez donc pas ce document chez nous, mais auprès du vendeur luukvaa. Stuvia facilite les paiements au vendeur.
Est-ce que j'aurai un abonnement?
Non, vous n'achetez ce résumé que pour €2,99. Vous n'êtes lié à rien après votre achat.
