Switch to: References

Add citations

You must login to add citations.
  1. Discretely ordered modules as a first-order extension of the cutting planes proof system.Jan Krajicek - 1998 - Journal of Symbolic Logic 63 (4):1582-1596.
    We define a first-order extension LK(CP) of the cutting planes proof system CP as the first-order sequent calculus LK whose atomic formulas are CP-inequalities ∑ i a i · x i ≥ b (x i 's variables, a i 's and b constants). We prove an interpolation theorem for LK(CP) yielding as a corollary a conditional lower bound for LK(CP)-proofs. For a subsystem R(CP) of LK(CP), essentially resolution working with clauses formed by CP- inequalities, we prove a monotone interpolation theorem (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Parametric Presburger arithmetic: complexity of counting and quantifier elimination.Tristram Bogart, John Goodrick, Danny Nguyen & Kevin Woods - 2019 - Mathematical Logic Quarterly 65 (2):237-250.
    Download  
     
    Export citation  
     
    Bookmark  
  • Some new results on decidability for elementary algebra and geometry.Robert M. Solovay, R. D. Arthan & John Harrison - 2012 - Annals of Pure and Applied Logic 163 (12):1765-1802.
    We carry out a systematic study of decidability for theories of real vector spaces, inner product spaces, and Hilbert spaces and of normed spaces, Banach spaces and metric spaces, all formalized using a 2-sorted first-order language. The theories for list turn out to be decidable while the theories for list are not even arithmetical: the theory of 2-dimensional Banach spaces, for example, has the same many-one degree as the set of truths of second-order arithmetic.We find that the purely universal and (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations