From: Leon Hansen <lhansen@uni-bremen.de>

Hello everybody,

I am currently writing my master thesis and I am trying to fetch entries

from a list that fulfil some properties. Similar to a query on a

database or an ontology.

My first approach looked like this:

datatype room = LivingRoom | Kitchen | SleepingRoom

consts connectedRooms:: "room ⇒ room ⇒ bool"

axiomatization where

a1: "connectedRooms LivingRoom Kitchen"

lemma patheval2: "connectedRooms X SleepingRoom"

nitpick[satisfy,show_consts,user_axioms] oops

In this case nitpick answers "X = LivingRoom" even though that is not

correct.

What can i do about that?

My other approach was to avoid axiomatisation completely and use

datatypes like this:

datatype ID = NewID nat

datatype Thing = Bed (height: nat) ID

definition bed1 where

"bed1 ≡ Bed 2 (NewID 1)"

definition bed2 where

"bed2 ≡ Bed 8 (NewID 3)"

definition bed3 where

"bed3 ≡ Bed 2 (NewID 5)"

definition bedList where

"bedList ≡ [bed1, bed2, bed3]"

lemma "List.filter (%c::Thing. ∃x. c = (Bed 2 (NewName x))) bedList =

res" nitpick sorry

However this becomes very slow for larger lists. Is there a way to do

this more efficiently?

Kind regards

Leon Hansen

From: "John F. Hughes" <jfh@cs.brown.edu>

I believe that the problem here is that you've specified what

"connectedRooms" does *only* when applied to LivingRoom and Kitchen, but

have not specified its value on any other pair of rooms. Nitpick says "Hey,

assigning "connectedRooms LivingRoom SleepingRoom" to be "true" is

consistent with all the axioms. I guess I'm done!"

So axiom 1 needs to be much richer --- either a complete enumeration of the

9 possibilities, or something with an "if" that says "if we're in this one

special case, then true; otherwise false."

NB: You could additionally specify a symmetry axiom ---

connectedRooms a b => connectedRooms b a [I'm forgetting the correct

syntax here]

and then safely have an enumeration of only 6 items instead of all 9.

-John

From: Leon Hansen <lhansen@uni-bremen.de>

I do have the reflexivity and transitivity in there already:

axiomatization where

refl: "connectedRooms x x" and

trans: "connectedRooms x y ∧ connectedRooms y z ⟶ connectedRooms x z"

I just shortend the example by a lot. For that reason it is not possible

to list every possibility as well.

I would need to add something like the "connectedRooms _ _ = False" that

would work if it were a function and not an axiomatisation.

-Leon

From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>

Dear Leon,

My first approach looked like this:

datatype room = LivingRoom | Kitchen | SleepingRoom

consts connectedRooms:: "room ⇒ room ⇒ bool"

axiomatization where

a1: "connectedRooms LivingRoom Kitchen"lemma patheval2: "connectedRooms X SleepingRoom" nitpick[satisfy,show_consts,user_axioms] oops

In this case nitpick answers "X = LivingRoom" even though that is not correct.

Although it doesn't correspond to your expectations, Nitpick's behavior is correct. Your "nitpick" command is asking for a model of the formula. Nitpick finds one. In that model, "connectedRooms LivingRoom SleepingRoom" is true. This is perfectly consistent with your axiomatization. It is not *entailed* by the axiomatization, but it is clearly consistent with it.

If you want to find a value X such that "connectedRooms X SleepingRoom" is provable -- in other words, a witness for X in "EX X. connectedRooms X SleepingRoom", I'm afraid there's no tool that will reliably give you that in Isabelle. The existential formula would be a candidate for Sledgehammer, but in general you wouldn't get the witness out of the proof.

Is there a way to do this more efficiently?

The problem is that I don't clearly understand what "this" refers to. I'm starting to suspect that your axiomatization above is wrong; you probably also want to say "~ connectedRooms LivingRoom SleepingRoom" etc., if you mean that these are not connected. (Otherwise, they'll be connected in some models of the formulas and not in others.)

Typically a better approach is to avoid low-level mechanisms such as "consts" and "axiomatization" and instead rely on the definitional mechanisms, like "inductive" (which is probably your best option here), "fun", and "definition". With "inductive", what you don't explicitly make true is automatically false, which is very convenient. You also don't need to worry about models; there's only one model.

I hope this helps.

Cheers,

Jasmin

From: Leon Hansen <lhansen@uni-bremen.de>

Dear Jasmin,

thank you for your detailed response.

If you want to find a value X such that "connectedRooms X SleepingRoom" is provable -- in other words, a witness for X in "EX X. connectedRooms X SleepingRoom", I'm afraid there's no tool that will reliably give you that in Isabelle. The existential formula would be a candidate for Sledgehammer, but in general you wouldn't get the witness out of the proof.

That confirmation is very helpful for me. I thought I was just doing it

completely wrong.

The problem is that I don't clearly understand what "this" refers to.

My goal is to embed knowledge from an owl ontology in an Isabelle theory

and be able to retrieve it again in reasonable time.

Typically a better approach is to avoid low-level mechanisms such as "consts" and "axiomatization" and instead rely on the definitional mechanisms, like "inductive" (which is probably your best option here), "fun", and "definition". With "inductive", what you don't explicitly make true is automatically false, which is very convenient. You also don't need to worry about models; there's only one model.

That is more or less what i did in my second approach where i used

"datatype" and "definition" only. Thank you for the tip with

"inductive". For small theories nitpick returns the requested

information reliably and fast. For theories with a few hundred lines it

was taking way to much time. I hoped there was a simple way to limit

nitpicks search space and speed up the search for witnesses for X in "EX

X. connectedRooms X SleepingRoom" for example.

Kind regards,

Leon

Last updated: Jul 15 2022 at 23:21 UTC