2017/05/24 by Matthias Horbach, Horbach, Matthias, Marco Voigt +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1705.08792
openalex publication_date 2017/05/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In general, first-order predicate logic extended with linear integer\narithmetic is undecidable. We show that the Bernays-Sch "onfinkel-Ramsey\nfragment (\∃^* \∀^*-sentences) extended with a restricted form of\nlinear integer arithmetic is decidable via finite ground instantiation. The\nidentified ground instances can be employed to restrict the search space of\nexisting automated reasoning procedures considerably, e.g., when reasoning\nabout quantified properties of array data structures formalized in Bradley,\nManna, and Sipma's array property fragment. Typically, decision procedures for\nthe array property fragment are based on an exhaustive instantiation of\nuniversally quantified array indices with all the ground index terms that occur\nin the formula at hand. Our results reveal that one can get along with\nsignificantly fewer instances.\n