모노딕 2차 논리

Monadic second-order logic

수학 논리학에서, 2차 논리(MSO)는 2차 논리 단편으로, 2차 양자화가 [1]집합의 양자화로 제한된다.그것은 특히 그래프의 논리학에서 중요하다. 왜냐하면 Courcelle의 정리 때문에, 그것은 유계 트리 폭의 그래프에 대한 모노딕 2차 공식을 평가하기 위한 알고리즘을 제공한다.그것은 또한 Büchi-Elgot-Trakhtenbrot 정리가 정규 언어의 논리적 특성을 제공하는 오토마타 이론에서 근본적으로 중요하다.

2차 로직에서는 술어보다 양화가 가능합니다.단, MSO는 2차 정량화가 모노딕 술어(인수가 1개인 프레딕트)로 제한되는 fragment입니다.이것은 종종 "집합"에 대한 수량화라고 설명되는데, 이는 모노딕 술어가 집합(술어가 참인 요소의 집합)에 대한 표현력에서 같기 때문이다.

변종

모노딕 2차 논리는 두 가지 변형이 있습니다.그래프나 Courcelle의 정리와 같은 구조에 대해 고려되는 변종에서 공식은 비단축 술어(이 경우 이진 에지 E Ey)\)를 포함할 수 있지만 정량화는 술어만을 사용하도록 제한됩니다.오토마타 이론과 Büchi-Elgot-Trahtenbrot 정리에서 고려되는 모든 술어는 등식( 과 순서 관계를 제외하고 단항이어야 한다.

평가의 계산 복잡성

EMSO(존재성 모노디컬 2차 논리)는 MSO의 fragment입니다.MSO에서는 집합 상의 모든 수량자가 공식의 다른 부분 이외의 존재 수량자여야 합니다.1차 수량자는 제한되지 않습니다.실존적(비단항적) 2차 논리가 복잡도 클래스 NP의 기술적 복잡성을 정확하게 포착하는 페이긴의 정리와 유사하게, 실존적 단항적 2차 논리로 표현될 수 있는 문제의 클래스는 단항 NP라고 불려왔다.단항 로직의 제한에 의해 비단항 2차 로직에서는 증명되지 않은 채로 있는 이 로직에서의 분리를 증명할 수 있습니다.예를 들어, 그래프의 논리에서는, 그래프의 나머지 부분과 연결되는 가장자리가 없는 정점의 적절한 서브셋의 존재를 설명하는 공식으로 나타낼 수 있기 때문에, 그래프의 연결 여부를 테스트하는 것은 단항 NP에 속합니다.그러나, 보충적인 문제, 그래프가 연결되어 있는지 테스트하는 것은 중단되지 않습니다.g to monadic NP.[2][3](단일 공식에 대한 제한 없이) 존재하는 2차 공식을 갖는 유사한 보완적 문제의 쌍이 존재하는 것은 계산 복잡성의 열린 질문인 NP와 coNP의 부등식과 동등하다.

반대로, 부울 MSO 공식이 입력 유한 트리에 의해 충족되는지 여부를 확인하고 싶을 때, 부울 MSO 공식을 트리 오토마톤으로[4] 변환하고 트리 상의 오토마톤을 평가함으로써 트리의 선형 시간 내에 이 문제를 해결할 수 있다.그러나 질의의 관점에서 이 프로세스의 복잡성은 일반적으로 [5]보충적이지 않다.Courcelle의 정리 덕분에 그래프의 트리 폭이 상수에 의해 제한된다면 입력 그래프에서 부울 MSO 공식을 선형 시간으로 평가할 수 있다.

입력 정보는 나무 또는 경계 treewidth는, 자유 변수가 있MSO의 공식을 들어,가 효율적으로 열거형 알고리즘 모든 solutions,[6]의 집합 입력 데이터 선형 시간을 각 해결책는 경우 지연 linear의 각 해결책의 크기, 즉, constant-delay에서 생산된다 preprocessed 것을 보장하는 생산.에서쿼리의 모든 자유 변수가 1차 변수인 일반적인 경우(즉, 집합을 나타내지 않음).이 [7]경우 MSO 공식의 솔루션 수를 계산하기 위한 효율적인 알고리즘도 있다.

만족도의 결정성 및 복잡성

이 논리는 1차 논리를 포함하기 때문에 모노딕 2차 논리에 대한 만족도 문제는 일반적으로 결정할 수 없습니다.

S2S라고 불리는 무한완성 이진 트리의 2차 원리는 결정 가능합니다.[8]이 결과로서 다음과 같은 이론이 결정될 수 있습니다.

  • 나무의 단일한 2차 이론.
  • 후계자(S1S) 하의N{N의 모나드 2차 이론.
  • wS2S 및 wS1S. 유한 서브셋(약한 모노딕 2차 로직)으로 한정합니다.이진수(서브셋으로 표시됨)의 경우 wS1S에서도 덧셈을 정의할 수 있습니다.

이러한 이론들(S2S, S1S, wS2S, wS1S) 각각에 대해, 의사결정 문제의 복잡성은 [5][9]보충적이지 않습니다.

검증 시 나무에 대한 MSO의 만족도 사용

트리의 Monadic 2차 논리는 결정성과 상당한 표현력 덕분에 소프트웨어 검증, 더 넓게는 형식 검증에 응용된다.만족도를 위한 의사결정 절차가 [10][11][12]구현되었다.이러한 절차는 하드웨어 [14]검증의 [13]상징적 추론뿐만 아니라 형태 분석의 한 형태로 링크된 데이터 구조를 조작하는 프로그램의 특성을 증명하기 위해 사용되었다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ Courcelle, Bruno; Engelfriet, Joost (2012-01-01). Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press. ISBN 978-0521898331. Retrieved 2016-09-15.
  2. ^ 를 클릭합니다Fagin, Ronald (1975), "Monadic generalized spectra", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21: 89–96, doi:10.1002/malq.19750210112, MR 0371623.
  3. ^ 를 클릭합니다Fagin, R.; Stockmeyer, L.; Vardi, M. Y. (1993), "On monadic NP vs. monadic co-NP", Proceedings of the Eighth Annual Structure in Complexity Theory Conference, Institute of Electrical and Electronics Engineers, doi:10.1109/sct.1993.336544, S2CID 32740047.
  4. ^ Thatcher, J. W.; Wright, J. B. (1968-03-01). "Generalized finite automata theory with an application to a decision problem of second-order logic". Mathematical Systems Theory. 2 (1): 57–81. doi:10.1007/BF01691346. ISSN 1433-0490. S2CID 31513761.
  5. ^ a b Meyer, Albert R. (1975). Parikh, Rohit (ed.). "Weak monadic second order theory of succesor is not elementary-recursive". Logic Colloquium. Lecture Notes in Mathematics. Springer Berlin Heidelberg: 132–154. doi:10.1007/bfb0064872. ISBN 9783540374831.
  6. ^ Bagan, Guillaume (2006). Ésik, Zoltán (ed.). "MSO Queries on Tree Decomposable Structures Are Computable with Linear Delay". Computer Science Logic. Lecture Notes in Computer Science. Springer Berlin Heidelberg. 4207: 167–181. doi:10.1007/11874683_11. ISBN 9783540454595.
  7. ^ Arnborg, Stefan; Lagergren, Jens; Seese, Detlef (1991-06-01). "Easy problems for tree-decomposable graphs". Journal of Algorithms. 12 (2): 308–340. doi:10.1016/0196-6774(91)90006-K. ISSN 0196-6774.
  8. ^ Rabin, Michael O. (1969). "Decidability of Second-Order Theories and Automata on Infinite Trees". Transactions of the American Mathematical Society. 141: 1–35. doi:10.2307/1995086. ISSN 0002-9947. JSTOR 1995086.
  9. ^ Stockmeyer, Larry; Meyer, Albert R. (2002-11-01). "Cosmological lower bound on the circuit complexity of a small problem in logic". Journal of the ACM. 49 (6): 753–784. doi:10.1145/602220.602223. ISSN 0004-5411. S2CID 15515064.
  10. ^ Henriksen, Jesper G.; Jensen, Jakob; Jørgensen, Michael; Klarlund, Nils; Paige, Robert; Rauhe, Theis; Sandholm, Anders (1995). Brinksma, E.; Cleaveland, W. R.; Larsen, K. G.; Margaria, T.; Steffen, B. (eds.). "Mona: Monadic second-order logic in practice". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. 1019: 89–110. doi:10.1007/3-540-60630-0_5. ISBN 978-3-540-48509-4.
  11. ^ Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš (2019-04-01). "Nested antichains for WS1S". Acta Informatica. 56 (3): 205–228. doi:10.1007/s00236-018-0331-z. ISSN 1432-0525. S2CID 57189727.
  12. ^ Traytel, Dmitriy; Nipkow, Tobias (2013-09-25). "Verified decision procedures for MSO on words based on derivatives of regular expressions". ACM SIGPLAN Notices. 48 (9): 3–f12. doi:10.1145/2544174.2500612. hdl:20.500.11850/106053. ISSN 0362-1340.
  13. ^ Møller, Anders; Schwartzbach, Michael I. (2001-05-01). "The pointer assertion logic engine". Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation. PLDI '01. Snowbird, Utah, USA: Association for Computing Machinery: 221–231. doi:10.1145/378795.378851. ISBN 978-1-58113-414-8. S2CID 11476928.
  14. ^ Basin, David; Klarlund, Nils (1998-11-01). "Automata based symbolic reasoning in hardware verification". Formal Methods in System Design. 13 (3): 255–288. doi:10.1023/A:1008644009416. ISSN 0925-9856.


Stub icon

이 논리 관련 기사는 stub입니다.위키피디아를 확장함으로써 위키피디아를 도울 수 있습니다.