arademaker / alc-lean Goto Github PK

Let us define some notations to simplify the code presentation. See https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html?highlight=infix#notation

We need notations for all concept constructors, subsumption of concepts and equivalence of concepts.

Symbols are already defined, we just need to make sure the syntax for notation and infix is updated to Lean 3.

1. The subsumption relation between concepts C and D is a linear order.
2. the equivalence between concepts C and D is an equivalence relation

Precisamos manter os exemplos atualizados. assumindo que ja temos predicados para T |= a onde a é um axioma do tipo C \subseteq D ou C \equiv D e T é um conjunto de axiomas (teoria), podemos ter um exemplo de T e a no arquivo de test. Possíveis exemplos são:

1. handbook DL pagina 56 figura 2.2 o exemplo da TBOX sobre família.
2. alguns exemplos em https://www.aifb.kit.edu/images/1/19/DL-Intro.pdf
3. algum exemplo do cap 9 do https://www.amazon.com/Knowledge-Representation-Reasoning-Artificial-Intelligence/dp/1558609326

ou qualquer outro exemplo que achar simples e interessante.