Stratified least fixpoint logic

DOI10.1016/0304-3975(94)90091-4zbMath0815.03018OpenAlexW2061373185MaRDI QIDQ1331926

Kevin J. Compton

Publication date: 1994

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

Full work available at URL: http://hdl.handle.net/2027.42/31383

zbMATH Keywords

expressibilitysequent calculuslogic programmingprogram verificationtotal correctnessdatabase queriesexistential least fixpoint logicstratified least fixpoint logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17)

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The expressive power of stratified logic programs
• Negation and control in PROLOG
• Proof theory. 2nd ed
• Proving total correctness of nondeterministic programs in infinitary logic
• Fixed point theorems and semantics: A folk tale
• Elementary induction on abstract structures
• Finiteness is mu-ineffable
• Program invariants as fixedpoints
• First-order dynamic logic
• Horn clause queries and generalizations
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• A Deductive System for Existential Least Fixpoint Logic
• An interpolation theorem for denumerably long formulas
• An axiomatic basis for computer programming
• Algorithmic properties of structures