We introduce a proof system for H´ ajek’s logic BL based on a relational hypersequents framework. We prove that the rules of our logical calculus, called RHBL, are sound and invertible with respect to any valuation of BL into a suitable algebra, called (ω)[0, 1]. Refining the notion of reduction tree that arises naturally from RHBL, we obtain a decision algorithm for BL provability whose running time upper bound is 2O(n), where n is the number of connectives of the input formula. Moreover, if a formula is unprovable, we exploit the constructiveness of a polynomial time algorithm for leaves validity for providing a procedure to build countermodels in (ω)[0, 1]. Finally, since the size of the reduction tree branches is O(n3), we can describe a polynomial time verification algorithm for BL unprovability.

Bova, S., Montagna, F. (2008). Proof Search in Hájek's Basic Logic. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 9, 1-26 [10.11145/1352582.1352589].

Proof Search in Hájek's Basic Logic.

MONTAGNA, FRANCO
2008-01-01

Abstract

We introduce a proof system for H´ ajek’s logic BL based on a relational hypersequents framework. We prove that the rules of our logical calculus, called RHBL, are sound and invertible with respect to any valuation of BL into a suitable algebra, called (ω)[0, 1]. Refining the notion of reduction tree that arises naturally from RHBL, we obtain a decision algorithm for BL provability whose running time upper bound is 2O(n), where n is the number of connectives of the input formula. Moreover, if a formula is unprovable, we exploit the constructiveness of a polynomial time algorithm for leaves validity for providing a procedure to build countermodels in (ω)[0, 1]. Finally, since the size of the reduction tree branches is O(n3), we can describe a polynomial time verification algorithm for BL unprovability.
2008
Bova, S., Montagna, F. (2008). Proof Search in Hájek's Basic Logic. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 9, 1-26 [10.11145/1352582.1352589].
File in questo prodotto:
File Dimensione Formato  
tocl-2008.pdf

non disponibili

Tipologia: Post-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 222.09 kB
Formato Adobe PDF
222.09 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11365/3563
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo