• A Syntactic characterization of bounded-rank decision trees in terms of decision lsts 

      Galesi, Nicola (1996-03-06)
      Report de recerca
      Accés obert
      Decision lists and decision trees are two models of computation for boolean functions. Blum has shown (Information Processing Letters 42 (1992), 183-185) that rank-k decision trees are a subclass of decision lists. ...
    • Exponential separation between tree-like and dag-like Cutting Planes proof systems 

      Bonet Carbonell, M. Luisa; Esteban Ángeles, Juan Luis; Galesi, Nicola; Johannsen, Jan (1997-12)
      Report de recerca
      Accés obert
      We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like ...
    • Linear lower bounds and simulations in Frege systems with substitutions 

      Bonet Carbonell, M. Luisa; Galesi, Nicola (1996-10)
      Report de recerca
      Accés obert
      Our work concerns Frege systems, substitution Frege systems (sF), renaming Frege systems, top/bottom-Frege systems and extended Frege systems (eF). Urquhart shows that tautologies associated to a binary strings ...
    • Monotone proofs of the pigeon hole principle 

      Atserias, Albert; Galesi, Nicola; Gavaldà Mestre, Ricard (2000-04)
      Report de recerca
      Accés obert
      We study the complexity of proving the Pigeon Hole Principle (PHP) in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We show that the standard encoding of the PHP as a monotone sequent admits ...
    • On the complexity of resolution with bounded conjunctions 

      Esteban Ángeles, Juan Luis; Galesi, Nicola; Messner, Jochen (2003-06)
      Report de recerca
      Accés obert
      We analyze size and space complexity of Res(k), a family of propositional proof systems introduced by Kraj which extend Resolution by allowing disjunctions of conjunctions of up to 1$ literals. We show that the ...
    • On vanishing sums of roots of unity in polynomial calculus and sum-of-squares 

      Bonacina, Ilario; Galesi, Nicola; Lauria, Massimo (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022)
      Text en actes de congrés
      Accés obert
      Vanishing sums of roots of unity can be seen as a natural generalization of knapsack from Boolean variables to variables taking values over the roots of unity. We show that these sums are hard to prove for polynomial ...
    • On vanishing sums of roots of unity in polynomial calculus and sum-of-squares 

      Bonacina, Ilario; Galesi, Nicola; Lauria, Massimo (2023-12)
      Article
      Accés obert
      We introduce a novel take on sum-of-squares that is able to reason with complex numbers and still make use of polynomial inequalities. This proof system might be of independent interest since it allows to represent multivalued ...
    • The Width-size method for general resolution is optimal 

      Bonet Carbonell, M. Luisa; Galesi, Nicola (1999-02)
      Report de recerca
      Accés obert
      The Width-Size Method for resolution was recently introduced by Ben-Sasson and Wigderson (BSW): Short Proofs are Narrow - Resolution Made Simple STOC 99). They found a trade-off between two complexity measures for ...