Looping proofs

Speaker(s)

Konrad Zdanowski

Affiliation

UKSW

Date

April 28, 2023, 12:15 p.m.

Room

room 5820

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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

---