Looping proofs

Prelegent(ci)

Konrad Zdanowski

Afiliacja

UKSW

Termin

28 kwietnia 2023 12:15

Pokój

p. 5820

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

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

---