A complete logic for reasoning about programs via nonstandard model theory. I

DOI10.1016/0304-3975(82)90004-4zbMath0475.68009OpenAlexW2063809508MaRDI QIDQ1159460

Ildikó Sain, Istvan Németi, Hajnalka Andréka

Publication date: 1982

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

Full work available at URL: https://doi.org/10.1016/0304-3975(82)90004-4

zbMATH Keywords

dynamic logicdecidable proof conceptfirst order dynamic languagestrongly complete inference system

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01) Nonstandard models (03H99)

Related Items (10)

Does “N+1 times” prove more programs correct than “N times”? ⋮ Changing a Semantics: Opportunism or Courage? ⋮ Output concepts for accelerated Turing machines ⋮ Unnamed Item ⋮ Temporal logics need their clocks ⋮ Reasoning in Dynamic Logic about Program Termination ⋮ On the Completeness of Dynamic Logic ⋮ Stability of weak second-order semantics ⋮ Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs? ⋮ The axiomatic semantics of programs based on Hoare's logic

Cites Work

• Applying modal logic
• Programs and program verifications in a general setting
• On some classes of interpretations
• Model theory for modal logic. Kripke models for modal predicate calculi
• First-order dynamic logic
• Model theory
• A practical decision method for propositional dynamic logic (Preliminary Report)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A complete logic for reasoning about programs via nonstandard model theory. I