가드 논리

Guarded logic

보호 논리는 결과가 제한적인 선택에 관련된 동적 논리의 선택 세트다.

보호 논리의 간단한 예는 다음과 같다:X가 참이면 Y, 그 외 Z는 (X?;)와 같이 동적 논리로 표현할 수 있다.Y)∪(~X?;Z).이것은 조심스러운 논리적인 선택을 보여준다: 만약 X가 버티면, 그렇다면 X?;;Y는 Y와 같고 ~X는?;Z는 차단되었고, Y yblock도 Y와 동일하다.따라서 X가 참일 때, 동작의 1차 수행자는 Y 분기만 취할 수 있고, 거짓일 때는 Z 분기만 취할 수 있다.[1]

현실 세계의 예는 역설의 개념이다: 무언가가 진실일 수도 거짓일 수도 없다.신중한 논리적인 선택은 진정한 의미의 변화가 모든 결정에 영향을 미치는 것이다.[2]

역사

보호 논리를 사용하기 전에는 모달 논리를 해석하는 데 크게 두 가지 용어가 사용되었다.수학논리와 데이터베이스론(인공지능)은 1차 술어 논리였다.두 용어는 모두 1등급 논리의 하위종류를 찾았으며 연구에 사용될 수 있는 해결 가능한 언어에서 효율적으로 사용된다.그러나 어느 쪽도 모달 스타일 로직에 대한 강력한 고정점 확장을 설명할 수 없었다.

후에 Moshe Y. Vardi는[3] 나무 모델이 많은 모달 스타일의 로직에서 효과가 있을 것이라고 추측했다.1차 논리학의 조심스러운 파편은 하날 안드레카, 이스탄 네메티, 요한 반 벤트헴이 그들의 기사 모달어와 경계 논리의 파편에서 처음 소개되었다.그들은 서술, 모달, 시간 논리의 핵심 속성을 술어 논리로 성공적으로 이전했다.보호 논리의 강력한 결정성은 나무 모델 속성으로 일반화될 수 있는 것으로 나타났다.트리 모델은 또한 보호 논리가 모달 로직의 기본을 유지하는 모달 프레임워크를 확장한다는 강력한 징후가 될 수 있다.

모달 로직은 일반적으로 이등분하여 침입하는 것이 특징이다.또한 이등분산 아래의 불변성이 자동자 이론의 정의에 도움이 되는 나무 모델 속성의 근원이 되는 경우도 있다.

보호 논리의 유형

지킴이 논리에는 수많은 지킴이 물체가 존재한다.첫번째로 보호되고 있는 파편은 모달 논리의 1차 논리학이다.보호되는 조각은 상대적인 정량화 패턴을 찾아 모달 정량화를 일반화한다.보호되는 파편을 나타내는 구문은 GF이다.또 다른 물체는 보호되는 고정점 논리로, μGF가 보호되는 파편을 최소점에서 최대점으로 자연적으로 확장한다.경계된 이등분할은 경계된 논리를 분석할 때 사용되는 물체다.약간 변형된 표준 관계 대수에서 보호되는 이등분율과 1차 순서 정의 가능한 모든 관계는 보호 관계 대수라고 알려져 있다.이것은 GRA를 사용하여 표시된다.

일차적 경계 논리 대상과 함께 이차적 경계 논리의 대상도 있다.'지킴이 2차 순서 논리'로 알려져 있고 GSO를 나타낸다. 2차 순서 논리와 유사하게, 지킴이 2차 순서 논리는 어느 범위보다 경계된 관계가 의미적으로 제한되는지를 계량한다.임의적 관계보다 범위가 제한되는 2차 논리와는 다르다.[4]

보호 논리의 정의

B를 우주 B와 어휘 τ과 관계 구조로 하자.

i) B에 X = {b_1, ..., b_k}의 접지 원자 α(b_1, ..., b_k)가 존재하면 X set B 세트가 B에 보호된다.

ii) subst 구조 A, 특히 하부 구조 A ⊆ B는 그 우주가 A(B)에 설정된 보호 구조일 경우 보호된다.

iii) 일부 경비원 집합 X ⊆ B에 대해 {b_1, ..., b_n} X가 되면 B에 투플 (b_1, ..., b_n) B^n이 보호된다.

iv) 튜플(b_1, ..., b_k) ∈ B^k는 구성 요소가 쌍으로 구별되어 있고 {b_1, ..., b_k}이(가) 보호 집합인 경우 B에서 보호 목록이다.빈 명단은 경호를 받는 명단이 된다.

v) 관계 X b B^n은 보호 튜플로만 구성될 경우 보호된다.[5]

가드 이등분

두 개의 τ구조물 A와 B 사이의 경계 이등분선은 앞뒤 조건이 만족되도록 A에서 B로 유한 부분 이등형 f: X → Y의 비빈 세트 I이다.

백: 모든 f: X → Y in I 및 모든 보호 세트 Y "B"에 대해 부분 이형 g: X" → Y"가 존재하므로, F^-1과 g^-1이 Y "Y"에 대해 동의한다.

포워드 f: X → Y in I 및 모든 보호대상 X의 ⊆ A에 대해 f와 g가 X에 동의하는 부분 이형 g: X" → Y"가 I에 존재한다.

참조

  1. ^ "Formal modeling and analysis of timed system". International Conference on Formal Modelling and Analysis of Timed Systems No4. Paris, France. September 25–27, 2006.
  2. ^ Nieuwenhuis, Robert; Andrei Voronkov (2001). Logic for Programming, Artificial Intelligence, and Reasoning. Springer. pp. 88–89. ISBN 3-540-42957-3.
  3. ^ Vardi, Moshe (1998). Reasoning about the Past with Two-Way Automata (PDF).
  4. ^ "Guarded Logics: Algorithms and Bisimulation" (PDF). pp. 26–48. Retrieved 15 May 2014.
  5. ^ "Guarded Logics: Algorithms and Bisimulation" (PDF). p. 25. Retrieved 15 May 2014.