An algebraic treatment of quantifier-free systems of arithmetic

被引:3
|
作者
Montagna, F [1 ]
机构
[1] UNIV SIENA,DIPARTIMENTO MATEMAT,I-53100 SIENA,ITALY
关键词
D O I
10.1007/s001530050042
中图分类号
O1 [数学];
学科分类号
0701 ; 070101 ;
摘要
By algebraic means, we give an equational axiomatization of the equational fragments of various systems of arithmetic. We also introduce a faithful semantics according to which, for every reasonable system T for arithmetic, there is a model where exactly the theorems of T are true.
引用
收藏
页码:209 / 224
页数:16
相关论文
共 50 条
  • [41] Coherence and Computational Complexity of Quantifier-free Dependence Logic Formulas
    Kontinen, Jarmo
    STUDIA LOGICA, 2013, 101 (02) : 267 - 291
  • [42] The Complexity of Limited Belief Reasoning-The Quantifier-Free Case
    Chen, Yijia
    Saffidine, Abdallah
    Schwering, Christoph
    PROCEEDINGS OF THE TWENTY-SEVENTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2018, : 1774 - 1780
  • [43] The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic
    Demri, Stephane
    Lozes, Etienne
    Mansutti, Alessio
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2021, 22 (02)
  • [44] DYNAMIC CONTACT ALGEBRAS AND QUANTIFIER-FREE LOGICS FOR SPACE AND TIME
    Dimitrov, Plamen
    Vakarelov, Dimiter
    SIBERIAN ELECTRONIC MATHEMATICAL REPORTS-SIBIRSKIE ELEKTRONNYE MATEMATICHESKIE IZVESTIYA, 2018, 15 : 1103 - 1144
  • [45] A quantifier-free SMT encoding of non-linear hybrid automata
    Cimatti, Alessandro
    Mover, Sergio
    Tonetta, Stefano
    PROCEEDINGS OF THE 12TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2012), 2012, : 187 - 195
  • [46] Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
    Stevens, Lukas
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 491 - 508
  • [47] Test selection criteria for quantifier-free first-order specifications
    Aiguier, Marc
    Arnould, Agnes
    Le Gall, Pascale
    Longuet, Delphine
    INTERNATIONAL SYMPOSIUM ON FUNDAMENTALS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4767 : 144 - +
  • [48] Deciding quantifier-free Presburger formulas using parameterized solution bounds
    Seshia, SA
    Bryant, RE
    19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 100 - 109
  • [49] Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions
    Alt, Leonardo
    Hyvaerinen, Antti E. J.
    Asadi, Sepideh
    Sharygina, Natasha
    PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), 2017, : 39 - 46
  • [50] Computational complexity of quantifier-free negationless theory of field of rational numbers
    Kossovski, N
    ANNALS OF PURE AND APPLIED LOGIC, 2002, 113 (1-3) : 175 - 180