Switch to: References

Add citations

You must login to add citations.
  1. Towards automated first-order abduction: the cut-based approach.Marcelo Finger - 2012 - Logic Journal of the IGPL 20 (2):370-387.
    Traditional abduction imposes as a precondition the restriction that the background information may not derive the goal data. In first-order logic such precondition is, in general, undecidable. To avoid such problem, we present a first-order cut-based abduction method, which has KE-tableaux as its underlying inference system. This inference system allows for the automation of non-analytic proofs in a tableau setting, which permits a generalization of traditional abduction that avoids the undecidable precondition problem. After demonstrating the correctness of the method, we (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  • Cut-Based Abduction.Marcello D'agostino, Marcelo Finger & Dov Gabbay - 2008 - Logic Journal of the IGPL 16 (6):537-560.
    In this paper we explore a generalization of traditional abduction which can simultaneously perform two different tasks: given an unprovable sequent Γ ⊢ G, find a sentence H such that Γ, H ⊢ G is provable ; given a provable sequent Γ ⊢ G, find a sentence H such that Γ ⊢ H and the proof of Γ, H ⊢ G is simpler than the proof of Γ ⊢ G . We argue that the two tasks should not be distinguished, (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • The cost of a cycle is a square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.
    The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with O(k n+l ) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Partially definable forcing and bounded arithmetic.Albert Atserias & Moritz Müller - 2015 - Archive for Mathematical Logic 54 (1):1-33.
    We describe a method of forcing against weak theories of arithmetic and its applications in propositional proof complexity.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Minimum propositional proof length is NP-Hard to linearly approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
    We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations