Once again, we have remembered the first level logic and have found that it has advantages and disadvantages.

The advantages are that it is very expressive, even if it is not everything you might want to express.

But on the other hand, it is sufficiently expressive to be indecisive.

From the standpoint of machine learning processing, this is not such a pleasant property.

It is not a complete killer.

You can still try to make a first-level knowledge representation in logic.

And many do that.

You can look for fragments, especially the horn fragment.

Horn fragment is simply programmed in Prolog.

And you can still build a medium-functioning theoretical proof for first-level logic.

So this is not a complete conclusion criterion.

But of course you would like to have knowledge representation formalisms,

of which you know that they are at least decidable.

So let's start again from the bottom.

We start with statements logic.

I will now remember this in detail in the rest of today's session.

We do this with the view of making algorithms.

You may ask yourself why I make algorithms and expression strength so elaborate for first-level logic.

And then the next logic comes in.

Statement logic and I suddenly only make algorithms and no more expression strength.

Why don't I make more expression strength here?

Everyone knows what statement logic is, even those who were not in Gleun.

So why do I not make statements logic with expression strength?

There is relatively little expression strength, but you can still ask yourself after the exact expression strength.

I'll leave it as a question.

I'll just put my memory here and answer the question again.

So, we want to make algorithms.

We want to look at three algorithms.

The good old resolution algorithm, which we also see in Gleun, is more or less a repetition.

But from this repetition we take out a lemma and from it we get the so-called backtracking algorithm for statement logic.

And if you optimize it a little bit, then you are at the so-called Davis-Putnam-Low-Gloveland algorithm.

And that is the one that is probably two-thirds of today's statement logic.

No, that does not mean that if you understand DPLL, you have understood how modern statement logic works.

They can do completely different things, but that is the rough basis.

And then we make another algorithm, the so-called tableau algorithm.

It plays no role in statement logic.

I don't know of any statement logic that works with tableau.

But we'll need that later.

Tableau can be expanded without compulsion on the statement logic that we are actually interested in later.

The common statement logic proofs are mostly tableau proofs in some form.

Okay.

So, as always, let's start with the syntax.

Very good. We should hopefully still know it.

So, a formula can be.

Yes, I'm doing it a little more extensive now than at the beginning in Gleunen.

So, I'm still taking up dual operators.

So, there is a sum of cases, there is a theorem, there is a conjunction, there is a disjunction, there is a negation.

And we can write down any propositional atoms, big A, big B and so on, from a fixed set.

I write script A.

I write it like this.