만족도

수학 논리학에서, 공식은 변수에 대한 값의 할당에서 참일 경우 만족할 수 있다. $x+3=y$ 를 들어, $x+3=y$ + $x+3=y$ $y=6$ y({ $displaystyle$ $x+3$ $=$ y $x+3=y$ })는 x $=$ 3({ $displaystyle$ x=3} $y=6$ y $y=6$ = 6({ $displaystyle$ y $=6$ 일 때 만족할 수 있지만, $x+1=x$ + 1 $x+1=x$ x { $displaystyle x+1$ x}은 만족할 수 없기 때문에 만족할 수 있습니다.만족도에 대한 이중 개념은 타당성입니다. 변수에 값을 할당할 때마다 공식이 참이 되는 경우 공식이 유효합니다.예를 들어 x $x+3=3+x$ + $x+3=3+x$ $x+3=3+x$ + $x+3=3+x$ ${\displaystyle$ x $+3=3+x}$ 는 $x+3=3+x$ 정수 위에 $x+3=y$ 하지만 $x+3=y$ x + $x+3=y$ $x+3=y$ {\ $displaystyle$ x $+3=y}$ 는 $x+3=y$ 유효하지 않습니다.

형식적으로는 1차 논리, 2차 논리 또는 명제 논리 등 허용되는 심볼의 구문을 정의하는 고정 논리에 관해 만족도를 연구한다.그러나, 만족도는 구문적이라기보다는, 예를 들어 x $x+1=x$ + $x+1=x$ $x+1=x$ $x+1=x$ {\ $displaystyle$ x $+1=x$ 와 $x+1=x$ 공식에서 $+(\displaystyle +)$ 의 $+$ 의미와 관련이 있기 때문에 의미적 속성이다. 우리는 해석(또는 모델)을 변수 및 변수에 대한 값 할당으로 정의한다.다른 모든 비논리적인 기호에 대한 의미부호 및 모든 해석에서 ^[1]참일 경우 공식이 만족스럽다고 한다.이를 통해 $+(\displaystyle$ $+$ 와 $+$ 같은 기호를 비표준적으로 해석할 수 있지만 추가 공리를 제공하여 의미를 제한할 수 있습니다.만족도 모듈로 이론은 (유한 또는 무한) 공리의 집합인 형식 이론에 대한 공식의 만족도를 고려합니다.

만족도와 타당성은 단일 공식에 대해 정의되지만, 임의의 이론이나 공식 세트로 일반화될 수 있습니다. 이론은 적어도 하나의 해석이 이론의 모든 공식을 참으로 만든다면 만족할 수 있고, 모든 공식이 모든 해석에서 참이라면 유효합니다.예를 들어, 페아노 산술과 같은 산술 이론은 자연수에서 참이기 때문에 만족할 수 있다.이 개념은 이론의 일관성과 밀접하게 관련되어 있으며, 사실 괴델의 완전성 정리라고 알려진 결과인 1차 논리의 일관성과 동등합니다.만족을 부정하는 것은 만족할 수 없는 것이고, 타당성을 부정하는 것은 무효이다.이 네 가지 개념은 아리스토텔레스의 반대편과 정확히 유사한 방식으로 서로 연관되어 있다.

명제논리에서의 공식이 만족스러운지를 결정하는 문제는 결정 가능하며, 부울 만족도 문제, 즉 SAT로 알려져 있다.일반적으로 1차 논리의 문장이 만족스러운지 여부를 판단하는 문제는 판단할 수 없다.보편 대수학, 등식 이론, 자동 정리 증명에서, 용어 개서, 일치 폐쇄 및 통일의 방법은 만족도를 결정하기 위해 사용된다.특정 이론이 결정 가능한지 여부는 그 이론이 가변성이 없는지와 다른 ^[2]조건에 따라 달라집니다.

유효성을 만족도로 낮추다

부정을 수반하는 고전 논리학의 경우, 위의 반대 제곱으로 표현된 개념들 사이의 관계 때문에 일반적으로 만족도를 수반하는 공식의 타당성에 대한 질문을 다시 표현할 수 있다.특히 is은 φ가 만족스럽지 못한 경우에만 유효하며, 즉 φ가 만족스러운 것은 거짓이다.바꿔 말하면, is이 무효인 경우에만 만족할 수 있습니다.

양의 명제 미적분과 같이 부정 없는 논리학의 경우, 타당성과 만족도에 대한 질문은 관련이 없을 수 있습니다.양의 명제 미적분의 경우, 모든 공식은 만족할 수 있는 반면, 타당성 문제는 co-NP 완전하기 때문에 만족성 문제는 사소한 것이다.

고전 논리에 대한 명제적 만족도

고전 명제 논리의 경우, 명제 공식에 대한 만족도는 결정될 수 있다.특히, 만족도는 NP-완전 문제이며, 계산 복잡도 이론에서 가장 집중적으로 연구되는 문제 중 하나이다.

1차 로직의 만족도

1차 논리(FOL)의 경우 만족도를 결정할 수 없습니다.보다 구체적으로 말하면, 이것은 공동 RE-완전 문제이기 때문에 반신반의할 ^[3]수 없습니다.이 사실은 FOL에 대한 유효성 문제의 결정 불가능성과 관련이 있습니다.유효성 문제의 현황에 대한 질문은 데이비드 힐버트에 의해 소위 "엔체이둥슈프로블럼"으로 처음 제기되었다.공식의 보편적 타당성은 괴델의 완전성 정리에 의해 반감정 가능한 문제이다.만약 만족도가 반감정 가능한 문제라면, 카운터 모델의 존재 문제도 마찬가지일 것이다(부정이 만족된다면 공식은 카운터 모델을 가진다).따라서 논리적 타당성의 문제는 결정될 수 있으며, 이는 교회-튜링 정리와 모순되며, 그 결과 "벤체이둥슈프로 문제"에 대한 부정적인 답을 기술한다.

모델 이론의 만족도

모형 이론에서, 원자식은 공식을 ^[4]참으로 만드는 구조의 요소들의 집합이 있다면 만족할 수 있다.A가 구조체이고, θ가 공식이고, a가 구조체로부터 θ를 만족시키는 요소의 집합인 경우, 일반적으로 다음과 같이 기술된다.

A ⊧ 、 [ a ]

has에 자유변수가 없는 경우, 즉 is가 원자문이고 A에 의해 충족되는 경우, 다음과 같이 기술합니다.

A ⊧

이 경우 A는 ,의 모델이라고 할 수도 있고 is은 ,의 모델이라고 할 수도 있다.T가 A가 만족하는 원자문(이론)의 집합체라면 다음과 같이 쓸 수 있다.

A t T

유한 만족도

만족도와 관련된 문제는 유한 만족도의 문제인데, 이것은 공식이 그것을 실현하는 유한한 모델을 허용하는지를 결정하는 문제이다.유한한 모델 특성을 가진 논리의 경우, 만족도와 유한한 만족도의 문제는 일치한다. 왜냐하면 그 논리의 공식은 유한한 모델을 가지고 있는 경우에만 모델을 가지고 있기 때문이다.이 질문은 유한 모형 이론의 수학 분야에서 중요하다.

유한 만족도와 만족도는 일반적으로 일치할 필요는 없다.예를 들어 다음 문장의 조합으로 얻을 수 있는 1차 논리식을 생각해 보겠습니다. $여기서$ $b$ 와 $a$ $b는$ 상수입니다.

$R(a_{0},a_{0})$
$R(a_{0,a_{1})$
$(\displaystyle\forall xy(R(x,y)\right 화살표\exists zR(y,z))}$
$\displaystyle \forall xyz(R(y,x)\wedge R(z,x)\rightarrow x=z)}$

결과 공식은 무한 $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ R $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ 0 , a $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ 0 $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ , $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ 1 $), ...({0}, a_$ {0 $}), R(a_{0}), R(a_$ {1}), R $(a_{1$ }, $a_$ {2 $}),$ \ldots $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ 입니다. $({displaystyle$ a_{0}}) 세 번째 공리로 존재해야 하는 원자({displaystyle R $})$ 는 $R$ 모델의 미세성을 위해 루프가 존재해야 하며, 이는 0 $({$ 0}) $a_{0}$ 다른 요소에 루프백하든 상관없이 네 번째 공리에 위배됩니다.

주어진 로직에서 입력식의 만족도를 결정하는 계산 복잡도는 유한 만족도를 결정하는 계산 복잡도와 다를 수 있습니다.실제로 일부 로직에서는 그 중 하나만 결정할 수 있습니다.

고전적인 1차 논리의 경우, 유한 만족도는 재귀적으로 열거할 수 있고(클래스 RE), 공식의 부정화에 적용되는 트라흐텐브로트의 정리에 의해 결정될 수 없다.

수치적 제약

수치적 제약은^[clarify] 수학 최적화 분야에서 종종 나타나는데, 수학 최적화 분야에서는 대개 일부 제약 조건의 대상이 되는 객관적 함수를 최대화(또는 최소화)하고자 한다.그러나 객관적인 함수는 차치하고, 단순히 제약조건이 충족 가능한지를 결정하는 기본적인 문제는 도전적이거나 결정되지 않을 수 있다.다음 표는 주요 사례를 요약한 것입니다.

제약	리얼을 넘다니다	정수 위에
선형	PTIME(선형 프로그래밍 참조)	NP-complete(정수 프로그래밍 참조)
다항식	예를 들어, 를 통해 결정될 수 있습니다.원통형 대수 분해	결정 불가능(힐버트의 10번째 문제)

테이블 소스: Bockmayr와 Weispfenning.^[5]^{: 754}

선형 구속조건의 경우 다음 표에 보다 완전한 그림이 제시되어 있습니다.

제약 사항:	합리화	정수	자연수
선형 방정식	PTIME	PTIME	NP-완전
선형 부등식	PTIME	NP-완전	NP-완전

테이블 소스: Bockmayr와 Weispfenning.^[5]^{: 755}

「」를 참조해 주세요.

메모들

^ 예를 들어 Boolos and Jeffrey, 1974, 11장을 참조하십시오.
^ Franz Baader; Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press. pp. 58–92. ISBN 0-521-77920-0.
^ Baier, Christel (2012). "Chapter 1.3 Undecidability of FOL". Lecture Notes — Advanced Logics. Technische Universität Dresden — Institute for Technical Computer Science. pp. 28–32. Archived from the original (PDF) on 14 October 2020. Retrieved 21 July 2012.
^ Wilifrid Hodges (1997). A Shorter Model Theory. Cambridge University Press. p. 12. ISBN 0-521-58713-1.
^ ^a ^b Alexander Bockmayr; Volker Weispfenning (2001). "Solving Numerical Constraints". In John Alan Robinson; Andrei Voronkov (eds.). Handbook of Automated Reasoning Volume I. Elsevier and MIT Press. ISBN 0-444-82949-0. (Elsevier) (MIT Press).

레퍼런스

불로스와 제프리, 1974년계산성과 논리성케임브리지 대학 출판부

추가 정보

Daniel Kroening; Ofer Strichman (2008). Decision Procedures: An Algorithmic Point of View. Springer Science & Business Media. ISBN 978-3-540-74104-6.
A. Biere; M. Heule; H. van Maaren; T. Walsh, eds. (2009). Handbook of Satisfiability. IOS Press. ISBN 978-1-60750-376-7.

[1] 예를 들어 Boolos and Jeffrey, 1974, 11장을 참조하십시오.

[2] Franz Baader; Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press. pp. 58–92. ISBN 0-521-77920-0.

[3] Baier, Christel (2012). "Chapter 1.3 Undecidability of FOL". Lecture Notes — Advanced Logics. Technische Universität Dresden — Institute for Technical Computer Science. pp. 28–32. Archived from the original (PDF) on 14 October 2020. Retrieved 21 July 2012.

[4] Wilifrid Hodges (1997). A Shorter Model Theory. Cambridge University Press. p. 12. ISBN 0-521-58713-1.

[BockmayrWeispfenning2001-5] Alexander Bockmayr; Volker Weispfenning (2001). "Solving Numerical Constraints". In John Alan Robinson; Andrei Voronkov (eds.). Handbook of Automated Reasoning Volume I. Elsevier and MIT Press. ISBN 0-444-82949-0. (Elsevier) (MIT Press).

[1]

[2]

[3]

[4]

[5]

Search

만족도

네임스페이스

더

목차

유효성을 만족도로 낮추다

고전 논리에 대한 명제적 만족도

1차 로직의 만족도

모델 이론의 만족도

유한 만족도

수치적 제약

「」를 참조해 주세요.

메모들

레퍼런스

추가 정보

Search

만족도

유효성을 만족도로 낮추다

고전 논리에 대한 명제적 만족도

1차 로직의 만족도

모델 이론의 만족도

유한 만족도

수치적 제약

「 」를 참조해 주세요.

메모들

레퍼런스

추가 정보

「」를 참조해 주세요.