5 papers
Theorem prover Arend
Fedor Part, Valery Isaev, Sergey Sinchuk
This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the…
Lower Bounds for Subset Sum in Resolution with Modular Counting
Fedor Part
In this paper we prove lower bounds for sizes of refutations of unsatisfiable vector Subset Sum instances $\overrightarrow{a}_1 x_1 + \dots + \overrightarrow{a}_n x_n = \overrighta…
First-Order Reasoning and Efficient Semi-Algebraic Proofs
Fedor Part, Neil Thapen, Iddo Tzameret
Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms: constant degree semi-algebra…
Resolution with Counting: Dag-Like Lower Bounds and Different Moduli
Fedor Part, Iddo Tzameret
Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), thi…
Semi-simplicial Types in Logic-enriched Homotopy Type Theory
Fedor Part, Zhaohui Luo
The problem of defining Semi-Simplicial Types (SSTs) in Homotopy Type Theory (HoTT) has been recognized as important during the Year of Univalent Foundations at the Institute of Ad…