Fixed points theorems for non-transitive relations

MaRDI QIDQ5028488zbMATH OpenFDO

Authors Jérémy Dubut, Akihisa Yamada

Publication date 9 February 2022

Full work available at URL https://arxiv.org/abs/2009.13065, https://lmcs.episciences.org/9055

zbMATH Keywords

fixed-pointsIsabelle/HOlattice theoryorder theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Fixed point theorems for spaces with a transitive relation
• Knaster-Tarski revisited
• A note on the Knaster-Tarski fixpoint theorem
• Monotone Relations, Fixed Points and Recursive Definitions
• scientific article; zbMATH DE number 1875952

Cites work

• A Brief Overview of Agda – A Functional Language with Dependent Types
• A formal proof of the Kepler conjecture
• A lattice-theoretical fixpoint theorem and its applications
• A Theorem on Partially Ordered Sets, With Applications to Fixed Point Theorems
• Chain-complete posets and directed sets with applications
• Fixed points and common fixed points theorems in pseudo-ordered sets.
• Formal proof - the four color theorem
• Grammar Analysis and Parsing by Abstract Interpretation
• scientific article; zbMATH DE number 1614689 (Why is no real title available?)
• scientific article; zbMATH DE number 3830849 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• scientific article; zbMATH DE number 3423547 (Why is no real title available?)
• scientific article; zbMATH DE number 7649979 (Why is no real title available?)
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Isabelle/HOL. A proof assistant for higher-order logic
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Sledgehammer: judgement day
• Some fixed point theorems for pseudo ordered sets
• Sur le théorème de Zorn
• The method of successive approximations for functional equations
• Trellis theory
• Weak chain-completeness and fixed point property for pseudo-ordered sets

Cited in

(1)

• scientific article; zbMATH DE number 6133342 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq
• Nitpick
• Isabelle/HOL
• PIDE
• Isabelle/jEdit
• HOL Light
• Sledgehammer
• Agda
• seL4

This page was built for publication: Fixed points theorems for non-transitive relations

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