TalkChess.com

As I sayed, this is more a vision than an idea. But let's see:

For humans many finals are clear won/lost or draw, after having a quick look on the table, although there are so many different variats to search. Why? Because when analysing the position, humans find out some axioms about the position. Then, based on these axioms, they make a kind of proof of how the win is possible or why not. For example, when the center is blocked and there are only kings and pawns, and the kings cannot walk beyound the enemy pawns, then people will recognise immediately that this is a draw, while an engine must first make a big search.

If we can formalize these kinds of axioms and also the win positions (all depending on position types), then we could use some theorem proving methods to prove that those kind of positions are (or are not) interesting - and at once we can characterize a whole class of them! Perhaps this knowledge can be somehow pre-computed (like today the end game table bases) and can just be used in end games. (I don't believe that in middle game the system is practicable - even if such axiomatic system would exist, it would be probably too complex to be used in limited time).

Simple heuristics (for end games) cab certainly help a lot, but you have to be careful: if the pattern is too general, then it will be applied in positions where it shouldn't be (exceptions) leading to inaccurate evaluation. On the other hand, if you're too rigid then the ebgine might score position A as a draw (say), but not position B, although it's "obvious" that the difference between them is insignificant (say, the attacker is to move in position A, but the defender is on move in position B and can make a move to reach position A). This doesn't sound so bad, but it'll actually cause a lot of problems in the search.

nionita wrote:As I sayed, this is more a vision than an idea. But let's see:

For humans many finals are clear won/lost or draw, after having a quick look on the table, although there are so many different variats to search. Why? Because when analysing the position, humans find out some axioms about the position. Then, based on these axioms, they make a kind of proof of how the win is possible or why not. For example, when the center is blocked and there are only kings and pawns, and the kings cannot walk beyound the enemy pawns, then people will recognise immediately that this is a draw, while an engine must first make a big search.

If we can formalize these kinds of axioms and also the win positions (all depending on position types), then we could use some theorem proving methods to prove that those kind of positions are (or are not) interesting - and at once we can characterize a whole class of them! Perhaps this knowledge can be somehow pre-computed (like today the end game table bases) and can just be used in end games. (I don't believe that in middle game the system is practicable - even if such axiomatic system would exist, it would be probably too complex to be used in limited time).

Yes, I consider this an important idea / approach. The main term here is "proof", IMO.

While one may try to build a new kind of heuristic in such a way, it has the potential for more: proving the status of a class of positions.

For my mate prover Chest I had some plans for such proofs, e.g. the kind of draw you describe, or for a kind of "wild queen", which chases the king of the opponent, and cannot be captured by that king, since otherwise the side with the queen would be stalemated and the game would be draw, which is exactly what we try to prove. This kind of "simple" patterns can be done by a kind of end game table computation.

It can be done, at least sometimes, what would be a start. The result, since it is a proof, is final, i.e. no further search is necessary.

Also, such kind of proof may help in situations, where normal search has great problems to come to the correct conclusion, like for fortresses. The nature of such positions is cyclic, which does not fit well the standard tree approach of the search.

Cheers, Heiner

hMx wrote: Yes, I consider this an important idea / approach. The main term here is "proof", IMO.

While one may try to build a new kind of heuristic in such a way, it has the potential for more: proving the status of a class of positions.

Yes, it must be a proof, otherwise it will not help because is looks like beeing very work intensive.

For my mate prover Chest I had some plans for such proofs, e.g. the kind of draw you describe, or for a kind of "wild queen", which chases the king of the opponent, and cannot be captured by that king, since otherwise the side with the queen would be stalemated and the game would be draw, which is exactly what we try to prove. This kind of "simple" patterns can be done by a kind of end game table computation.

It can be done, at least sometimes, what would be a start. The result, since it is a proof, is final, i.e. no further search is necessary.

Also, such kind of proof may help in situations, where normal search has great problems to come to the correct conclusion, like for fortresses. The nature of such positions is cyclic, which does not fit well the standard tree approach of the search.

If we could identify - in a given position - which are the key pieces and the key fields, then the rest does not matter, and this can be easy represented and then we can easy check during the search if we reached that class of position - and we know the result.

Cheers, Heiner

Nicu

nionita wrote:As I sayed, this is more a vision than an idea. But let's see:

For humans many finals are clear won/lost or draw, after having a quick look on the table, although there are so many different variats to search. Why? Because when analysing the position, humans find out some axioms about the position. Then, based on these axioms, they make a kind of proof of how the win is possible or why not. For example, when the center is blocked and there are only kings and pawns, and the kings cannot walk beyound the enemy pawns, then people will recognise immediately that this is a draw, while an engine must first make a big search.

If we can formalize these kinds of axioms and also the win positions (all depending on position types), then we could use some theorem proving methods to prove that those kind of positions are (or are not) interesting - and at once we can characterize a whole class of them! Perhaps this knowledge can be somehow pre-computed (like today the end game table bases) and can just be used in end games. (I don't believe that in middle game the system is practicable - even if such axiomatic system would exist, it would be probably too complex to be used in limited time).

It wouldn't hurt if you first investigate which knowledge most programs actually posses.

As for Diep it has all knowledge, but probably the engines you're using they have rather simple evaluation function, from chess knowledge viewpoint.

Basically they have a table for each piece on each square and they have a value for each piece. Both for opening and for endgame. Then they have a bonus for a passed pawn and that's about it.

So what you all write would be interesting for Diep and 0 other engines.

Thanks,
Vincent