3 - Nonclassical Logics in Computer Science [ID:10801]
50 von 676 angezeigt

Given conjunctive normal form is valid.

So I've heard that you already have the solution.

So maybe you just want to explain it.

Maybe in front.

Yep. Actually, we should maybe.

So the question from the lecture before the last one was,

how are those to determine if a conjunctive normal form is valid?

So a conjunctive normal form is a conjunction of clauses.

So a conjunctive normal form is valid if all the clauses of

that conjunctive normal form are valid.

A clause is valid if the clause is a distinction of literals or negated literals.

And a clause is valid if it contains at least one literal in negated form and a non-negated form.

If it contains one literal in a negated and non-negated form, yeah, it's valid.

So all you have to do to determine if a conjunctive normal form is valid,

check all the clauses.

If they are valid, then to check all the clauses,

you just have to skip over all literals and determine,

yeah, do they occur negated and negated.

And if you found one, you can stop.

And yet if you exhausted all the space, you know it's not valid.

So how hard is it?

It's the number of clauses in the conjunctive normal form

times the number of literals in the clauses,

maybe literals of the clauses squared depends on how you would implement the check

if a literal of course negated and non-negated.

Thanks.

How many of you were in complexity of algorithms?

Used to be basic lecture.

Okay, that's enough.

So basically we've heard an argument that this is doable and polynomial time.

Can we do better?

Was that a stab at an answer or did it catch you?

Logarithmic space in fact suffices.

Yeah.

So basically you have to store indices of the current value of what you are looking for.

Right.

And so basically as a reminder to those, or reminder, well as a bit of additional complexity

theory for those who haven't been in complexity of algorithms,

there is a fairly important complexity class called L.

I mean the short name sort of gives away how important it is.

Of problems solvable in logarithmic space.

So actually in less space than the input.

Of course that can only work if you don't actually count the space where you store the

input in your overall space consumption.

So this is a Turing machine model with two tapes.

So this here is the input tape and this here is the work tape.

So the input resides on the input tape which to be fair is read only so you cannot cheat

and actually write into your input and clandestinely remember things by overwriting your input.

And the space counted is only the one on the work tape.

So logarithmic space is the class of problems that can be solved by only logarithmic space

Zugänglich über

Offener Zugang

Dauer

01:31:04 Min

Aufnahmedatum

2015-10-20

Hochgeladen am

2019-04-28 08:19:02

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