Prelegent: Konrad Zdanowski

Oto autorskie streszczenie referatu:

Opowiem o pracy A. Atseriasa i M. Laurii, w której autorzy analizują dowody w klasycznym rachunku zdań, w których grafy dowodu mogą być cykliczne, tzn. możemy, na przykład, użyć  dowodzonej formuły jako jednej z przesłanek w kroku dowodu. Autorzy pokazują, że w pewnych systemach dowodzenia, takich jak rezolucja, możliwość taka skraca wykładniczo długość dowodów.

 
A. Atserias and M. Lauria.
Circular (Yet Sound) Proofs.
ACM Transactions on Computational Logic, Volume 24, Issue 3, Article No.: 20, pp. 1–26, 2023.
https://www.cs.upc.edu/~atserias/papers/circular-proofs/circular-proofs.pdf