[Rochus]

This discussion started already in the sixties (see e.g. the 1969 publication by McCarthy and Hayes where they describe the "frame problem" as a fundamental obstacle to the attempt to model the dynamic world using First-Order Logic and monotonic reasoning). A popular attempt to "solve" this problem is the Cyc project. Monotonic logic is universally understood as a special, restricted case (a subset) of a broader non-monotonic theory.

[mycall]

I'm familiar with Cyc but never considered it a monotonic reasoning, but it definitely makes sense in retrospect. It appears Lean Machines [0] is a step head, combining both sides of the frame problem as a specific, although it likely leans towards leans (pun intended).

[0] https://github.com/lean-machines-central/lean-machines

[Rochus]

Thanks for the hint. The "LeanMachines" project literally seems to recreate Event-B constructs (contexts, machines, events, and refinement proof obligations) inside the Lean 4 proof assistant (using Lean 4 as a "host language").