You are not logged in |
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
