13 - Nonclassical Logics in Computer Science [ID:10811]
50 von 455 angezeigt

Music

Last time is to discuss the...

...whether we really need all those connectives, right? Because in classical logic...

...in classical logic we didn't really need so many of them.

Well, we already noted that no double negation holds so many of the transformations that we are able to do...

...in classical logic will not be valid intuitionistically. Maybe let's do one more example.

So I stressed the pressure over invocation so it's probably easy to guess that it is not defined in terms of other connectives...

...but we would like to have a proof. So our question is, is it true that alpha 5 times psi is intuitionistically the same?

Well, I didn't define what it is, but this we can keep for our own definition, conjunction of two implications, right?

So is it really the same intuitionistically that...

...is it the same thing as not phi or psi?

And...

...well, what do you think? Does it have a chance to fall...

My cross-section might be one of the places where...

...it's recording my heartbeat.

It's better now?

So, it had a chance that it would fall in one direction.

So we really have two questions here.

That's question number one.

And question number two is whether...

If you think carefully about this one.

So, this can be true at a given point if...

...remembering the definition of this junction, if one of these two guys is true.

So let's first say that psi is true.

It means that psi should be true everywhere above.

Which should guarantee by the two implications, right?

It doesn't even matter whether your successor, whatever successor you are choosing is satisfying phi or not.

It has to satisfy psi anyway, if we're taking the right contract.

What if non-phi is true?

Well, then this means that nowhere above phi is true.

So the implication that we have as definition for implication, universal quantified one...

...is vacuously true because it has false antecedent.

It is never the case for anything that is above our point.

Let's say w, for any w prime above it, that phi will be true here.

So if the definition for implication was saying that...

...anywhere above, wherever phi is true, psi has to be true.

Well, it's very easy to satisfy because phi is never true.

So this holds.

How about this one?

Well, let's think about a very simple instance where we take just atoms to be.

Do you remember the counter model that we had yesterday?

What if I say make AB go here?

So let's recall the definition.

I'm using AB and I was using AB for the names of those points.

The points we named x and y.

Y was the one above?

Y was...

So let's recall the definition.

So let's recall the definition, nxy and our accessibility relation, a pos order was consisting of xx, yy, xy.

And now I'm saying PA is the same as PB.

Zugänglich über

Offener Zugang

Dauer

01:28:40 Min

Aufnahmedatum

2015-11-24

Hochgeladen am

2019-04-28 03:49:03

Sprache

en-US

The course overviews non-classical logics relevant for computer scientists, in particular

  • Modal logics, extended to formalisms for reasoning about programs - PDL, mu-calculus. Modal systems also form the core of logics of agency and logics for reasoning about knowledge. Moreover they can be seen as a computationally well-behaved fragment of first-order logic over relational structures.

  • Intuitionistic logic, which can be seen as a fragment of certain modal logics (S4) or as the logic of type theory and program extraction.

  • Linear logic, which is established as the core system for resource-aware reasoning 

  • The logic of bunched implications and separation logic: more recent formalisms to reason about heap verification and programs involving shared mutable data structures.

  • Fuzzy and multi-valued logics for reasoning with vague information.

Einbetten
Wordpress FAU Plugin
iFrame
Teilen