Bernays – Schönfinkel 클래스
Bernays–Schönfinkel class폴 버네이스(Paul Bernays), 모제스 쇤핀켈(Moses Schönfinkel), 프랭크 램지(Frank P. Ramsey)의 이름을 딴 공식의 버네이스-쇤핀켈 클래스(Bernays-Schönfinkel-Ramsey 클래스)는 만족도가 결정 가능한 1차 논리 공식의 일부입니다.
이것은 프레넥스 정규 형식으로 작성될 때 ∃ ∗ ∀ ∗{\ \exists ^{*}\forall ^{*} 한정자 접두사를 가지며 함수 기호를 포함하지 않는 문장 집합입니다.
이러한 종류의 논리 공식은 근거화 또는 인스턴스화 과정에 의해 명제 논리 공식으로 효과적으로 번역될 수 있기 때문에 효과적으로 명제화(EPR)라고도 합니다.
이 수업의 만족도 문제는 NEXPTIME-완전입니다.[1]
적용들
EPR의 만족도를 결정하는 효율적인 알고리즘이 SMT 솔루션에 통합되었습니다.[2]
참고 항목
메모들
- ^ Lewis, Harry R. (1980), "Complexity results for classes of quantificational formulas", Journal of Computer and System Sciences, 21 (3): 317–353, doi:10.1016/0022-0000(80)90027-6, MR 0603587
- ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (eds.). "Deciding Effectively Propositional Logic Using DPLL and Substitution Sets". Automated Reasoning. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 410–425. doi:10.1007/978-3-540-71070-7_35. ISBN 978-3-540-71070-7.
참고문헌
- Ramsey, F. (1930), "On a problem in formal logic", Proc. London Math. Soc., 30: 264–286, doi:10.1112/plms/s2-30.1.264
- Piskac, R.; de Moura, L.; Bjorner, N. (December 2008), "Deciding Effectively Propositional Logic with Equality" (PDF), Microsoft Research Technical Report (2008–181)
