Email Gateway (Aug 23 2022 at 08:16): Email Gateway (Aug 23 2022 at 08:16):From: David MENTRÉ <David.MENTRE@bentobako.org>
Hello,
Context: I am a software engineer and private company researcher working
with formal methods. While I have some experience with formal tools like
Abstract Interpretation on industrial software, I never used proof
assistants like Isabelle/HOL or Coq. I came to Isabelle/HOL through
discussion with other users (advocating its tooling) and through the
book "Concrete Semantics" by Nipkow and Klein. I am interested in trying
to use Isabelle/HOL to formalize some basic English text and in
particular software requirements using predicate logic. In particular, I
would like to write documents combining informal English text and its
formal counterpart.
I successfully installed Isabelle/HOL 2019 and started to play with it.
While there is a lot of documentation and examples, I nonetheless had
some issues to define the right approach to work in a defined logical
context (i.e. define some predicates, some axioms, ...) due to the
richness of Isabelle/HOL.
In the end, it seems that using "locale" is the good(?) way, illustrated
by below example theory:
"""
theory example
imports Main
begin
typedecl person
locale my_context =
fixes parent :: "person ⇒ person ⇒ bool"
fixes ancestor :: "person ⇒ person ⇒ bool"
fixes related :: "person ⇒ person ⇒ bool"
assumes parent_is_ancestor : "∀x y. parent x y ⟶ ancestor x y"
assumes ancestor_of_ancestor_is_ancestor :
"∀ x z.∃ y. ancestor x y ∧ ancestor y z ⟶ ancestor x z"
assumes related: "∀x y. related x y = (∃z. ancestor z x ∧ ancestor z y)"
begin
lemma " parent a b ∧ parent a c ⟶ related b c"
using parent_is_ancestor related by auto
lemma "True"
by auto
end
end
"""
After this experiment, I have several questions.
Q1: Are there examples (perhaps as part of lessons on logic) of English
text with corresponding Isabelle/HOL formalization? I would like to
copy/paste and imitate typical formalization patterns. "Concrete
Semantics" is a good source, but it is focused on computer languages. I
am interested in more general models of daily life texts.
Q2: Is the above approach using "locale" the correct way to do this kind
of formalization? Is there a simpler way?
Q3: A big risk when defining axioms is to quickly produce
inconsistencies. Is there any good methodology or recommended approach
to avoid such inconsistencies? For example book "A Proof Assistant for
Higher-Order Logic" by Nipkow, Paulson and Wenzel recommend to use
"datatype" and "primrec" to avoid such inconsistencies. I could not find
how to use them to reason in above simple example.
Q4: Where is the documentation related to writing documents with
Isabelle/HOL, typically like AFP entries with pretty-printing, ...? I
have no problem using LaTeX if needed.
Best regards,
D. Mentré
Email Gateway (Aug 23 2022 at 08:16):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear David,
For general purpose on mixing English and formal Isabelle artefacts, I
encourage you to take a look on:
[1]
https://ore.exeter.ac.uk/repository/bitstream/handle/10871/38402/Isabelle_DOF-1.0.0_Isabelle2019.pdf?sequence=1&isAllowed=y
[1] has also an application on a certification standard, where textual
requirements in English are mixed with formal Isabelle artefacts such as
lemmas, definitions, etc
Another application on mixing formal and informal content in order to
assure security requirements for cyber physical systems, and uses [1] and
Isabelle is:
[2] https://link.springer.com/chapter/10.1007/978-3-030-34968-4_21
In [2] an assurance case pattern on the use formal artefacts in assurance
cases is proposed.
Best wishes,
Yakoub.
Email Gateway (Aug 23 2022 at 08:16):From: Alexandre Rademaker <arademaker@gmail.com>
Hi David,
I am not sure if your question is:
Your example suggests that you are looking for advising on the (2) above, am I right? I have done a simple experiment on the formalization of a TPTP problem in Lean; if you are interested, I can share the link with you. Not relevant for this mailing list, maybe.
In another direction, you could want to take a look at semantic representation structures from computational linguistics such as AMR, MRS, etc. These are intermediary structures used to represent the semantics of a natural language sentence. Try some sentences in http://erg.delph-in.net and see the output. These are not formal logical language but a step to it.
I am not very fluent in Isabelle, but things obvious for the knowledge representation people, like the representation of classes and class hierarchy, have a not so clear counterpart in dependent-types. Maybe somehow related to the https://en.wikipedia.org/wiki/Expression_problem?!
Best,
Email Gateway (Aug 23 2022 at 08:16):From: David MENTRÉ <David.MENTRE@bentobako.org>
Hello Alexandre and Yakoub,
Le 31/01/2020 à 04:03, Alexandre Rademaker a écrit :
I am not sure if your question is:
- about the technicalities of mix formal language and informal language on the same document or
This was my question Q4 but this is not the core of my question. But
this part nonetheless interests me. I am part of projects with
certification aspects. As usual, people are using Word/Excel approach
but I do think having a formal layout of the certification case
arguments could be beneficial, in the spirit of "Evidencial Tool Bus" of
John Rushby. Therefore thanks Yakoub for providing me reminder about
Isabelle/DOF. I saw the announcement... but forgot about it. :-)
- related to the formalization of English sentences, probably involving common-sense knowledge, in interactive theorem provers like Isabelle, Coq, Lean...
Your example suggests that you are looking for advising on the (2) above, am I right?
Yes, this is exactly the core of my questions Q1, Q2 and Q3.
I have done a simple experiment on the formalization of a TPTP problem in Lean; if you are interested, I can share the link with you. Not relevant for this mailing list, maybe.
Yes, please send me your link.
In another direction, you could want to take a look at semantic representation structures from computational linguistics such as AMR, MRS, etc. These are intermediary structures used to represent the semantics of a natural language sentence. Try some sentences in http://erg.delph-in.net and see the output. These are not formal logical language but a step to it.
I am not very fluent in Isabelle, but things obvious for the knowledge representation people, like the representation of classes and class hierarchy, have a not so clear counterpart in dependent-types. Maybe somehow related to the https://en.wikipedia.org/wiki/Expression_problem?!
I am less interested in formal representation of natural language or
knowledge.
I am more interested at building a formal model of a system or
requirements described as English text using human expertise. I
understand each formalization is probably specific to each system
description, but nonetheless there might be patterns or best practices
(typically to avoid inconsistencies). I'm looking for such patterns or
best practices, preferably in Isabelle/HOL, but examples in Lean or Coq
or other formal systems also interests me.
Best regards,
david
Last updated: Apr 25 2024 at 16:19 UTC