형식언어,formal_language



MKLINK
명세,specification
formalization_method // 혹은 이것자체를 mv to formalization Srch:formalization
bmks
Formal Methods Wiki
https://formalmethods.fandom.com/wiki/Formal_Methods_Wiki

Key ppl:
Eric_Hehner WpEn:Eric_Hehner
{
다음 비디오에서 다룸... 20분. 논리,logic산술,arithmetic을 어떻게 결합할 것인가
How to unify logic & arithmetic - YouTube
https://www.youtube.com/watch?v=niqqm1DRTkE


먼저 symbols:
⊤ \top WtEn: -> largest
⊥ \bot WtEn: -> smallest

binary logic에 순서,order 주기, (=ordering)?
∧ AND
⊥ ∧ ⊤ = ⊥
AND ∧
⊥ < ⊤
and : minimum

∨ OR
⊥ ∨ ⊤ = ⊤
OR ∨
or : maximum

반대인 top/bot 기호는 위아래반대로.
commutative operation인 and/or 기호를 좌우대칭으로. (의도된 것)

x<4 ⇒ x<6
이건
(x<4) is stricter than→ (x<6),
(x<4) is less true than→ (x<6)
로 볼 수 있다. 그렇다면
⊥ → … → (x<4) → (x<6) → … → ⊤
여기서 가장 오른쪽에 있는 ⊤가 '정리,theorem' 지위를 가진다.
‘When a 진술,statement is true(top), we call it a theorem.’

⊥ → −∞ (false → negative infinity)
T → +∞ (true → positive infinity)

$\displaystyle \sum$ 대신 $\displaystyle +\langle ... \rangle$
$\displaystyle \prod$ 대신 $\displaystyle \times\langle ... \rangle$

그 외 많고 특히 표기법,notation에 대한 many clever ideas. etc.
PL syntax design에 helpful

}



Intr:








}