The axiomatization of override and update

DOI10.1016/J.JAL.2009.11.001MaRDI QIDQ975885zbMATH OpenOpenAlexFDO

Authors Jasper Berendsen, David N. Jansen, Julien Schmaltz, F. Vaandrager

Publication date 11 June 2010

Published in Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2066/83911

zbMATH Keywords

automated deductioncompletenessSMT solversfunction algebraoverridingequational logic

Mathematics Subject Classification ID

Relational systems, laws of composition (08A02) Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05)

Recommendations

• Override and update
• Skew lattices and binary operations on functions
• The algebra of functions with antidomain and range
• An axiomatic theory for partial functions
• An axiomatization of partial n-place operations

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 3936465 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 3501559 (Why is no real title available?)
• scientific article; zbMATH DE number 194916 (Why is no real title available?)
• A new approach to the maximum-flow problem
• Compositional Abstraction in Real-Time Model Checking
• Isabelle/HOL. A proof assistant for higher-order logic
• Model theory.
• Subsumption of the Theory of Boolean Algebras under the Theory of Rings
• The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)

Cited in

(10)

• Skew lattices and binary operations on functions
• Residuated skew lattices
• Override and restricted union for partial functions
• Difference-restriction algebras of partial functions with operators: discrete duality and completion
• Difference-restriction algebras of partial functions: axiomatisations and representations
• Override and update
• How to generalise demonic composition
• My journey into noncommutative lattices and their theory
• The algebra of functions with antidomain and range
• A non-commutative Priestley duality.

Describes a project that uses

Uses Software

• Z
• Yices
• Isabelle/HOL

This page was built for publication: The axiomatization of override and update

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