The implementation of a logic requires, besides the definition of a calculus and a decision procedure, the development of techniques to reduce the search space. In this paper we introduce some simplification rules for Intuitionistic propositional logic that try to replace a formula with an equi-satisfiable ``simpler'' one with the aim to reduce the search space. Our results are proved via semantical techniques based on Kripke models. We also provide an empirical evaluation of their impact on implementations.

Simplification Rules for Intuitionistic Propositional Tableaux

FERRARI, MAURO;
2012

Abstract

The implementation of a logic requires, besides the definition of a calculus and a decision procedure, the development of techniques to reduce the search space. In this paper we introduce some simplification rules for Intuitionistic propositional logic that try to replace a formula with an equi-satisfiable ``simpler'' one with the aim to reduce the search space. Our results are proved via semantical techniques based on Kripke models. We also provide an empirical evaluation of their impact on implementations.
tableau calculi; simplification; intuitionistic logic
File in questo prodotto:
File Dimensione Formato  
2012-f3-constantSignOptimization-tocl.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: DRM non definito
Dimensione 1.26 MB
Formato Adobe PDF
1.26 MB 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: http://hdl.handle.net/11383/1756897
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 8
social impact