Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Aktualności — Wydarzenia

SLIWOWICA

 

Looping proofs


Prelegent: Konrad Zdanowski

2023-04-28 12:15

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