Number of the records: 1
Algebraic proofs over noncommutative formulas
- 1.
SYSNO ASEP 0374819 Document Type J - Journal Article R&D Document Type Journal Article Subsidiary J Článek ve WOS Title Algebraic proofs over noncommutative formulas Author(s) Tzameret, Iddo (MU-W) SAI Source Title Information and Computation. - : Elsevier - ISSN 0890-5401
Roč. 209, č. 10 (2011), s. 1269-1292Number of pages 24 s. Language eng - English Country US - United States Keywords proof complexity ; algebraic proof systems ; frege proofs Subject RIV BA - General Mathematics R&D Projects LC505 GA MŠMT - Ministry of Education, Youth and Sports (MEYS) CEZ AV0Z10190503 - MU-W (2005-2011) UT WOS 000295019700001 EID SCOPUS 80052231047 DOI 10.1016/j.ic.2011.07.004 Annotation We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege, yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analog of Frege proofs, different from that given in Buss et al. (1997) and Grigoriev and Hirsch (2003). We then turn to an apparently weaker system, namely, polynomial calculus (PC) where polynomials are written as ordered formulas (PC over ordered formulas, for short). Given some fixed linear order on variables, an arithmetic formula is ordered if for each of its product gates the left subformula contains only variables that are less-than or equal, according to the linear order, than the variables in the right subformula of the gate. Workplace Mathematical Institute Contact Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757 Year of Publishing 2012
Number of the records: 1