Julius Hamilton (Apr 10 2024 at 03:03): Julius Hamilton (Apr 10 2024 at 03:03):Hey,
I am exploring different ways to make formally verifiable models of any given system. I’m interested in category theory as well, functional ologs and relational ologs. I cannot yet see clearly exactly what format my envisioned model would take. This is an attempt to show the thinking process.
When you make an Olog, you can kind of start anywhere, and by drawing more and more relationships, get a better idea of what the overall structure of your model will be.
So then we could start anywhere. For example, a restaurant has customers, dishes on its menu, operating costs, infrastructure needs, an address, opening hours, and much else. Each of those in turn has its own attributes and properties.
I so far feel like the two fundamental ways of defining things in Coq is either with the record keyword or the inductive keyword.
Does anyone think they know a good way in Coq to write a basic olog? Also, could anyone show examples of what kinds of properties of a system could be verified, this way?
Last updated: Oct 13 2024 at 01:02 UTC