Order:
  1. A Tableau Calculus for Propositional Intuitionistic Logic with a Refined Treatment of Nested Implications.Mauro Ferrari, Camillo Fiorentini & Guido Fiorino - 2009 - Journal of Applied Non-Classical Logics 19 (2):149-166.
    Since 1993, when Hudelmaier developed an O-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and F c with a new set of rules to treat signed formulas of the kind T → C) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search and the width of proofs (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  2. A Secondary Semantics for Second Order Intuitionistic Propositional Logic.Mauro Ferrari, Camillo Fiorentini & Guido Fiorino - 2004 - Mathematical Logic Quarterly 50 (2):202-210.
    In this paper we propose a Kripke-style semantics for second order intuitionistic propositional logic and we provide a semantical proof of the disjunction and the explicit definability property. Moreover, we provide a tableau calculus which is sound and complete with respect to such a semantics.
    Direct download  
     
    Export citation  
     
    Bookmark  
  3. New Tableau Characterizations for Non-Clausal MaxSAT Problem.Guido Fiorino - 2022 - Logic Journal of the IGPL 30 (3):422-436.
    In this paper, we provide non-clausal tableau calculi for the maximum satisfiability problem and its variants. We discuss both basic calculi to characterize the problem and their modifications to reduce the proof size.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark