A logic covering undefinedness in program proofs
From MaRDI portal
Publication:790610
DOI10.1007/BF00264250zbMATH Open0534.68024OpenAlexW2089387242MaRDI QIDQ790610FDOQ790610
Publication date: 1984
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00264250
General topics in the theory of software (68N01) Other nonclassical logic (03B60) Abstract data types; algebraic specification (68Q65)
Cites Work
- Edinburgh LCF. A mechanized logic of computation
- Partial abstract types
- An introduction to the PL/CV2 programming logic
- On a Formalization of the Non-Definedness Notion
- Separation properties and Boolean powers
- The Calculus of Partial Predicates and Its Extension to Set Theory I
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (44)
- Reasoning about Separation Using Abstraction and Reification
- Process algebra with four-valued logic
- Many-valued logic and mixed integer programming
- Two over three: a two-valued logic for software specification and validation over a three-valued predicate calculus
- Bunch theory: axioms, logic, applications and model
- Title not available (Why is that?)
- A note on undefined expression values in programming logics
- Natural 3-valued logics—characterization and proof theory
- An algebraic expression of finite horizon optimal control algorithm for stochastic logical dynamical systems
- On solvability of systems of partial fuzzy relational equations
- Partial Functions and Equality in Answer Set Programming
- Proof obligations for blocks and procedures
- A guided tour of the mathematics of MetaSoft '88
- A first order logic for partial functions
- Partial logics reconsidered: A conservative approach
- Kleene's three-valued logic and process algebra
- Truth versus information in logic programming
- Partiality and recursion in interactive theorem provers – an overview
- Inversive meadows and divisive meadows
- Analysis of spatio-temporal properties of stochastic systems using TSTL
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- A simple sequent calculus for partial functions
- A logical framework for evolving software systems
- A first order logic for partial functions
- Proof systems for reasoning about computation errors
- Weak logic theory
- Simple consequence relations
- A typed logic of partial functions reconstructed classically
- General correctness: A unification of partial and total correctness
- Empowering the Event-B method using external theories
- Reasoning About Incompletely Defined Programs
- Modular structuring of VDM specifications in VVSL
- A two-valued logic for properties of strict functional programs allowing partial functions
- Preservation of properties of residuated algebraic structure by structures for the partial fuzzy set theory
- A completeness proof for a regular predicate logic with undefined truth value
- Ours Is to Reason Why
- Partial-predicate logic in computer science
- Quasi-boolean equivalence
- The connection between two ways of reasoning about partial functions
- Missing values and dragonfly operations in fuzzy relational compositions
- Using typed lambda calculus to implement formal systems on a machine
- Why the constant ‘undefined’? Logics of partial terms for strict and non-strict functional programming languages
- Efficient Well-Definedness Checking
- Partial functions and logics: A warning
Uses Software
This page was built for publication: A logic covering undefinedness in program proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q790610)
