Summary Modelling Computing Systems Extra notities Faron Moller & Georg Struth
14 views 0 purchase
Course
Logic For Computer Science (INFOB1LI)
Institution
Universiteit Utrecht (UU)
Logic for Computer Science/ Computer Technology Logic. Summary of the notes given by the teacher. This substance is tested next to the book Modelling Computing Systems for the exam. Given at Utrecht University.
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.
The benefits of buying summaries with Stuvia:
Guaranteed quality through customer reviews
Stuvia customers have reviewed more than 700,000 summaries. This how you know that you are buying the best documents.
Quick and easy check-out
You can quickly pay through credit card or Stuvia-credit for the summaries. There is no membership needed.
Focus on what matters
Your fellow students write the study notes themselves, which is why the documents are always reliable and up-to-date. This ensures you quickly get to the core!
Frequently asked questions
What do I get when I buy this document?
You get a PDF, available immediately after your purchase. The purchased document is accessible anytime, anywhere and indefinitely through your profile.
Satisfaction guarantee: how does it work?
Our satisfaction guarantee ensures that you always find a study document that suits you well. You fill out a form, and our customer service team takes care of the rest.
Who am I buying these notes from?
Stuvia is a marketplace, so you are not buying this document from us, but from seller luukvaa. Stuvia facilitates payment to the seller.
Will I be stuck with a subscription?
No, you only buy these notes for $3.21. You're not tied to anything after your purchase.
