An algebraic treatment of quantifier-free systems of arithmetic

被引：3
|
作者：
Montagna, F [1 ]
机构：
[1] UNIV SIENA,DIPARTIMENTO MATEMAT,I-53100 SIENA,ITALY
来源：
ARCHIVE FOR MATHEMATICAL LOGIC | 1996年 / 35卷 / 04期
关键词：
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 条
  • [1] Interpolating Quantifier-Free Presburger Arithmetic
    Kroening, Daniel
    Leroux, Jerome
    Ruemmer, Philipp
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2010, 6397 : 489 - +
  • [2] An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
    Angelo Brillout
    Daniel Kroening
    Philipp Rümmer
    Thomas Wahl
    Journal of Automated Reasoning, 2011, 47 : 341 - 367
  • [3] Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
    Brillout, Angelo
    Kroening, Daniel
    Ruemmer, Philipp
    Wahl, Thomas
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2011, 6538 : 88 - +
  • [4] An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
    Brillout, Angelo
    Kroening, Daniel
    Ruemmer, Philipp
    Wahl, Thomas
    JOURNAL OF AUTOMATED REASONING, 2011, 47 (04) : 341 - 367
  • [5] An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
    Brillout, Angelo
    Kroening, Daniel
    Ruemmer, Philipp
    Wahl, Thomas
    AUTOMATED REASONING, 2010, 6173 : 384 - +
  • [6] Deciding Quantifier-free Definability in Finite Algebraic Structures
    Campercholi, Miguel
    Tellechea, Mauricio
    Ventura, Pablo
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2020, 348 : 23 - 41
  • [7] Quantifier-free descriptions for interval-quantifier linear systems
    Sharaya, I. A.
    TRUDY INSTITUTA MATEMATIKI I MEKHANIKI URO RAN, 2014, 20 (02): : 311 - 323
  • [8] Quantifier-free encoding of invariants for hybrid systems
    Cimatti, Alessandro
    Mover, Sergio
    Tonetta, Stefano
    FORMAL METHODS IN SYSTEM DESIGN, 2014, 45 (02) : 165 - 188
  • [9] Quantifier-free encoding of invariants for hybrid systems
    Alessandro Cimatti
    Sergio Mover
    Stefano Tonetta
    Formal Methods in System Design, 2014, 45 : 165 - 188
  • [10] MonadicNLIN and quantifier-free reductions
    Lautemann, C
    Weinzinger, B
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 1999, 1683 : 322 - 337
12345