On strictly arithmetical completeness in logics of programs

DOI10.1016/0304-3975(91)90336-ZMaRDI QIDQ2277248zbMATH OpenOpenAlexFDO

Authors Andrzej Szałas

Publication date 1991

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(91)90336-z

zbMATH Keywords

algorithmic logicconcurrent dynamic logiclogics of programsstrictly arithmetical completeness of an axiom systemstrictly arithmetical interpretationstemporal logic

Mathematics Subject Classification ID

Logic in computer science (03B70)

Review text

A notion of strictly arithmetical completeness of an axiom system is introduced as the completeness w.r.t. strictly arithmetical interpretations. An interpretation is called to be strictly arithmetical if it contains the sort of natural numbers (with 0, 1, \(+\), and *), while all other of its sorts are effectively encodable by natural numbers. Thus strictly arithmetical interpretations form a proper subclass of the arithmetical ones (considered by David Harel and others). The author proposes a uniform technique to obtain the strictly arithmetical complete axiomatization for logics of programs, and exemplifies it by systems for algorithmic logic, concurrent dynamic logic, and temporal logic.

Recommendations

• On arithmetical completeness of the logic of proofs
• On completeness of logic programs
• Arithmetical Completeness of the Intuitionistic Logic of Proofs
• scientific article; zbMATH DE number 1989643
• Strict completion of logic programs
• On the proofs of arithmetical completeness for interpretability logic
• scientific article; zbMATH DE number 1567841
• scientific article; zbMATH DE number 3878896
• Arithmetic complexity of the predicate logics of certain complete arithmetic theories
• scientific article; zbMATH DE number 3869303

Cites work

• A complete logic for reasoning about programs via nonstandard model theory. II
• Arithmetical axiomatization of first-order temporal logic
• Concerning the semantic consequence relation in first-order temporal logic
• Concurrent dynamic logic
• First-order dynamic logic
• scientific article; zbMATH DE number 3985193 (Why is no real title available?)
• scientific article; zbMATH DE number 4057487 (Why is no real title available?)
• scientific article; zbMATH DE number 3558938 (Why is no real title available?)
• scientific article; zbMATH DE number 3577197 (Why is no real title available?)
• scientific article; zbMATH DE number 3637823 (Why is no real title available?)
• scientific article; zbMATH DE number 3799616 (Why is no real title available?)
• Incompleteness of first-order temporal logic with until
• On static logics, dynamic logics, and complexity classes
• Some relationships between logics of programs and complexity theory
• Soundness and Completeness of an Axiom System for Program Verification

Cited in

(12)

• Arithmetical completeness versus relative completeness
• Axiomatizing fixpoint logics
• A theory of strict P-completeness
• Program schemes, arrays, Lindström quantifiers and zero-one laws
• A simplified proof of arithmetical completeness theorem for provability logic GLP
• A Function Elimination Method for Checking Satisfiability of Arithmetical Logics
• On the Completeness of Dynamic Logic
• A Complete Axiomatization of Computer Arithmetic
• scientific article; zbMATH DE number 3968566 (Why is no real title available?)
• scientific article; zbMATH DE number 732053 (Why is no real title available?)
• scientific article; zbMATH DE number 1882007 (Why is no real title available?)
• Strict completion of logic programs

This page was built for publication: On strictly arithmetical completeness in logics of programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2277248)