arXiv subjects

Avgerinos Delkos

Publications and source records attributed to Avgerinos Delkos.

3 recordsLinked to original sources

arXiv2025

Prover-Adversary games for systems over (non-deterministic) branching programs

We introduce Pudlak-Buss style Prover-Adversary games to characterise proof systems reasoning over deterministic branching programs (BPs) and non-deterministic branching programs (NBPs). Our starting points are the proof systems eLDT and eLNDT, for BPs and NBPs respectively, previously introduced by Buss, Das and Knop. We prove polynomial equivalences between these proof systems and the corresponding games we introduce. This crucially requires access to a form of negation of branching programs which, for NBPs, requires us to formalise a non-uniform version of the Immerman-Szelepcsenyi theorem that coNL = NL. Thanks to the techniques developed, we further obtain a proof complexity theoretic version of Immerman-Szelepcsenyi, showing that eLNDT is polynomially equivalent to systems over boundedly alternating branching programs.

cs.CC↗

arXiv2025

Proof complexity of positive branching programs

We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, just like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC1, respectively. The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT+ is obtained by restricting their systems to a positive syntax, similarly to how the 'monotone sequent calculus' MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas. Our main result is that eLNDT+ polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudlák, that was recently improved to a bona fide polynomial simulation via works of Jeřábek and Buss, Kabanets, Kolokolova and Koucký. Along the way we formalise several properties of counting functions within eLNDT+ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.

cs.CC↗

arXiv2025

A significance-based account of ceteris paribus counterfactuals

When evaluating a counterfactual statement, it is often convenient to specify conditions that ought to be kept unchanged. Formally, this can be done by associating to each counterfactual a ceteris paribus set of formulas, specifying the facts that "ought to be kept unchanged". Ceteris paribus counterfactuals originate in the debate between D. Lewis and Fine in the 1970s, and have been captured in formal accounts. However, these accounts are merely based on 'counting' formulas, and can yield counterintuitive results. In this paper, we develop a novel approach to evaluate ceteris paribus counterfactuals at (weakly) centered sphere models, by taking into account the 'significance' of formulas that ought to be kept unchanged. Hypothetical states that keep the most significant formulas unchanged will be prioritized in the evaluation of a counterfactual. We show that the resulting notion of validity coincides with theoremhood in Lewis' conditional logics VC or VW.

cs.LO↗