nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
1,312 Commits 32 Branches 0 Tags 62 MiB
Commit Graph

1312 Commits

Author SHA1 Message Date
Nicolas Méric 68417e01d3 Update invariants-section 2022-02-04 15:10:46 +01:00
Nicolas Méric 30793f5c51 Update invariants section 2022-02-04 15:08:47 +01:00
Nicolas Méric 35a117a361 Ugly fix for expansion of class antiquotations 2022-02-04 09:11:53 +01:00
Nicolas Méric 09129bfbf8 Update titlerunning and clean up text 2022-02-03 15:19:09 +01:00
Idir AIT SADOUNE 8663703d53 Adding invariants to the PLIB example 2022-02-03 14:15:01 +01:00
Nicolas Méric 2e645ed5ff Update structure of Advanced Evaluation section 2022-02-03 11:33:56 +01:00
Burkhart Wolff 092d552ef8 fixed bugs 2022-02-03 11:30:22 +01:00
Nicolas Méric 927f0446a0 Update invariants section 2022-02-03 11:04:39 +01:00
Idir AIT SADOUNE b0a29ac00d Adding a text explaining the interest of the ontology mapping. 2022-02-03 10:17:33 +01:00
Idir AIT SADOUNE 4b43756eb3 Merge branch '2021-ITP-PMTI' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF into 2021-ITP-PMTI 2022-02-03 09:15:22 +01:00
Idir AIT SADOUNE 4936a8142e Un update of the PLIB example 2022-02-03 09:14:53 +01:00
Nicolas Méric 7033335e3f Update extensible record section 
Update text to reflect that a property apply on the scheme type
of the record
 2022-02-03 09:06:10 +01:00
Nicolas Méric a2f3057545 Update extensible record section 
Make it compile
 2022-02-03 09:00:53 +01:00
Burkhart Wolff e6721b548d added 2 sections in background. 2022-02-02 23:04:37 +01:00
Burkhart Wolff d319ab2555 section on extensible records 2022-02-02 17:03:17 +01:00
Nicolas Méric 502f5c5cd2 Switch to lipics template and update invariants section 2022-02-02 12:43:51 +01:00
Nicolas Méric 7ac669e52e Update invariants section 2022-01-31 17:38:37 +01:00
Nicolas Méric d9f2d5c0c4 Merge branch 'master' into 2021-ITP-PMTI 2022-01-31 13:09:26 +01:00
Nicolas Méric 8f7e898f4b Fix invariant railroad diagram 2022-01-31 13:01:59 +01:00
Burkhart Wolff ae96c7cef0 Merge branch 'master' into 2021-ITP-PMTI 2022-01-31 10:52:41 +01:00
Burkhart Wolff e650892b48 changed 'L' - operator to 'Lang' in order to avoid name conflicts in papers. 2022-01-31 10:44:02 +01:00
Burkhart Wolff 35b47223b9 added category 'background' into scholarly paper 2022-01-31 10:42:52 +01:00
Achim D. Brucker 46325cc64b Added unofficial support for lipics-v2021 (warning: this requires a patched version of lipics-v2021.cls). 2022-01-30 22:52:48 +00:00
Burkhart Wolff 9d9fd03b72 minor stuff 2022-01-30 20:59:21 +01:00
Burkhart Wolff b243f30252 changed 'L' - operator to 'Lang' in order to avoid name conflicts in papers. 2022-01-30 20:57:59 +01:00
Burkhart Wolff 05b896291b ... 2022-01-30 14:56:22 +01:00
Burkhart Wolff cc151291f6 some figures on MathTaxonomies 2022-01-30 14:55:19 +01:00
Burkhart Wolff 3e06e659b6 global restructuring 2022-01-30 14:50:22 +01:00
Burkhart Wolff eaef236dcc added category 'background' into scholarly paper 2022-01-30 14:48:54 +01:00
Burkhart Wolff b35c774d27 polished intro 2022-01-30 13:47:18 +01:00
Burkhart Wolff c5cdf5f826 revised introduction 2022-01-29 22:27:30 +01:00
Nicolas Méric a38d13198c Add invariants and queries draft in 2021-ITP-PMTI 2022-01-28 17:18:09 +01:00
Idir AIT SADOUNE f8c125bcff Engineering Example extracted from a PLIB example 2022-01-28 14:28:54 +01:00
Burkhart Wolff 9cd021d7fa new paper structure 2022-01-26 11:53:00 +01:00
Burkhart Wolff 9d7fc957c6 new syntax for paper. And the future. 2022-01-26 11:17:22 +01:00
Burkhart Wolff b1fb509d8b Modifs of title and abstract 2022-01-26 11:16:32 +01:00
Burkhart Wolff 63145e0d3a Merge branch '2021-ITP-PMTI' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF into 2021-ITP-PMTI 2022-01-26 09:24:29 +01:00
Burkhart Wolff be0352cab7 ... 2022-01-26 09:24:20 +01:00
Nicolas Méric 6d42f122b1 Merge branch 'master' into 2021-ITP-PMTI 2022-01-25 08:52:52 +01:00
Nicolas Méric d546a714b7 Merge pull request 'Add checking of invariants for class instances' (#8) from nicolas.meric/Isabelle_DOF:check-invariants-first-draft into master 
Reviewed-on: Isabelle_DOF/Isabelle_DOF#8
 2022-01-25 07:50:25 +00:00
Nicolas Méric 76612ae6f3 Add checking of invariants for class instances 
- Warning: the current implementation does yet not support
    some use-cases, like invariant on monitors,
    or the initialization of docitem without a class associated.
- Add first draft of the checking of invariants.
  For now, it is disabled by default because some cases
  are not yet supported, like the initialization of docitem
  without a class associated.
  ex: text*[sdf]‹ Lorem ipsum @{thm refl}›
- To enable the checking, one can use the theory attribute
  "invariants_checking" by declaring it in a theory like this:
  declare [[invariants_strict_checking = true]]
- A checking using basic tactics (unfolding and auto) can be enable
  with the "invariants_checking_with_tactics" theory attribute
  for specific use-cases
- The specification of invariants is now automatically abstracted,
  so one must define an invariant like this now:

  doc_class W =
  w::"int"
  invariant w :: "w σ ≥ 3"

  The old form:

  doc_class W =
  w::"int"
  invariant w :: "λσ. w σ ≥ 3"

  is now deprecated.
  The specification of the invariant still uses the σ-notation
  and is defined globally by the name component "invariantN"
- Update the invariants definition in the theories to match
  the new implementation
- Update the manual to explain this new feature
- Add small examples in src/tests/High_Level_Syntax_Invariants.thy
  and src/tests/Ontology_Matching_Example.thy
 2022-01-24 17:30:48 +01:00
Burkhart Wolff e53984feea Merge branch '2021-ITP-PMTI' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF into 2021-ITP-PMTI 2022-01-20 22:08:38 +01:00
Burkhart Wolff d7c7a98138 added elements to related work: OntoMathPro, ScienceWISE, DBpedia 2022-01-20 22:08:32 +01:00
Idir AIT SADOUNE 8629dda85e first version of a case study 2022-01-20 10:59:17 +01:00
Nicolas Méric 688e823463 Make 2021-ITP-PMTI paper compile 2022-01-19 09:40:05 +01:00
Burkhart Wolff 96112ff893 restored ancient SEFM paper example for invariants 2022-01-17 12:06:32 +01:00
Burkhart Wolff 5631010371 added figures from IFM 19 paper 2022-01-14 15:31:15 +01:00
Burkhart Wolff 68e9f64156 added figures from talk 2022-01-13 16:24:07 +01:00
Burkhart Wolff 647f8e86cc Reorg / shoprtening chap 2. 2022-01-11 20:53:07 +01:00
Burkhart Wolff b5939bc9db added basckground chapter . First flush. 2022-01-08 22:22:22 +01:00