ファイル置き場 Sendai Logic Homepage

Resolution for first order logic

藤原 誠

東北大学理学研究科数学専攻

2010.11.5東北大学ロジックセミナー

Introduction

Satisfiability problem is one of decision problems.

If we resolve this problem,

we could also resolve Valid problem, Consequence

problem, and Equivalence problem.

The subject of my talk is to decide unsatisfiability of

first-order sentence, automatically by a computer.

I rewrite the condition that a first-order sentence ϕ

is satisfiable one after another to be more simple

form .

Introduction

Satisfiability problem is one of decision problems.

If we resolve this problem,

we could also resolve Valid problem, Consequence

problem, and Equivalence problem.

The subject of my talk is to decide unsatisfiability of

first-order sentence, automatically by a computer.

I rewrite the condition that a first-order sentence ϕ

is satisfiable one after another to be more simple

form .

Definition.

A formula is inSNFif it has the form∀x1...∀xnψwhereψis a conjunction of disjunctions of literals.

Fact.1

For any formulaϕof first-order logic, we can find a formulaϕ^S in SNF such thatϕis satisfiable⇔ ϕ^S is satisfiable by simple automatic operations.

For any formulaϕin SNF, we define a formula that does not use equality.

Definition.

A formula is inSNFif it has the form∀x1...∀xnψwhereψis a conjunction of disjunctions of literals.

Fact.1

For any formulaϕof first-order logic, we can find a formulaϕ^S in SNF such thatϕis satisfiable⇔ ϕ^S is satisfiable by simple automatic operations.

For any formulaϕin SNF, we define a formula that does not use equality.

Definition.

A formula is inSNFif it has the form∀x1...∀xnψwhereψis a conjunction of disjunctions of literals.

Fact.1

For any formulaϕof first-order logic, we can find a formulaϕ^S in SNF such thatϕis satisfiable⇔ ϕ^S is satisfiable by simple automatic operations.

For any formulaϕin SNF, we define a formula that does not use equality.

Definition.

V :vocabulary ofϕ, E :binary relation that is not inV ϕ, ≡the sentence obtained by replacing each occurrence of

t1= t2^inϕwithE(t1^,t2).

ϕ_ER≡ ∀x∀y∀z[E(x, y) ∧ (E(x, y) ↔ E(y, x)) ∧ (E(x, y) ∧ E(y, z) → E(x, z))] ϕ_R ≡ ∀x∀y∀z^[(∧n_i=1E(xi^,yi) ∧ R(x1^{, ...,}xn)⁾→ R(y1^{, ...,}yn)^]

ϕ₁ ≡ ^∧

R∈V

ϕ_R

ϕ_f ≡ ∀x₁...∀x_n∀y₁∀y_n^[∧n_i=1E(x_i,y_i) → E ( f (x₁, ...,x_n), f (y₁, ..,y_n))^] ϕ₂ ≡ ^∧

f ∈V

ϕ_f

ϕ_E ≡ (ϕ,∧ ϕER∧ ϕ1∧ ϕ2)^S

Fact.2

For any SNF sentenceϕ,

ϕis satisfiable ⇔ ϕE is satisfiable.

Definition.

V :vocabulary ofϕ, E :binary relation that is not inV ϕ, ≡the sentence obtained by replacing each occurrence of

t1= t2^inϕwithE(t1^,t2).

ϕ_ER≡ ∀x∀y∀z[E(x, y) ∧ (E(x, y) ↔ E(y, x)) ∧ (E(x, y) ∧ E(y, z) → E(x, z))] ϕ_R ≡ ∀x∀y∀z^[(∧n_i=1E(xi^,yi) ∧ R(x1^{, ...,}xn)⁾→ R(y1^{, ...,}yn)^]

ϕ₁ ≡ ^∧

R∈V

ϕ_R

ϕ_f ≡ ∀x₁...∀x_n∀y₁∀y_n^[∧n_i=1E(x_i,y_i) → E ( f (x₁, ...,x_n), f (y₁, ..,y_n))^] ϕ₂ ≡ ^∧

f ∈V

ϕ_f

ϕ_E ≡ (ϕ,∧ ϕER∧ ϕ1∧ ϕ2)^S

Fact.2

For any SNF sentenceϕ,

ϕis satisfiable ⇔ ϕE is satisfiable.

Definition.

LetV be a vocabulary.

HerbrandV-structureisV-structure that hasH(V)as

universe and interprets the constans and relations in natural way,where H(V)is the set of all variable freeV-term.

It is regardless of how the relations are interpreted. H(V)is calledHerbrand universeforV.

Example.

LetV = { f (arity : 1), R(arity : 2), c}^. Then,H(V) = {c, f (c), f ( f (c)), ...}^. M = (H(V)| f, R, c)^,

which interpretcand f in natural way andRas{(c, c), (c, f (c))}, be a HerbrandV-structure.

Definition.

Let_Γbe a set of sentences.

Herbrand modelof_Γis HerbrandV_Γ-structure that models_Γ, where V_Γ is the set of constants, functions, and relations in_Γ. (If_Γcontains no constant, we add one constant inV_Γ)

In the case where _Γcontains a single sentenceϕ, we will replace_Γin the above notion withϕ.

H(V_ϕ)is calledHerbrand universeofϕ.

Let SNF sentenceϕbe∀x₁...∀xnϕ0(x1...xn), whereϕ0 is quantifier-free and equality free.

Then,

E(ϕ) := {ϕ^{0(t1, ...,tn)|t1, ...,tn ∈ H(Vϕ)}.}

Theorem.1

For any equality-free SNF sentenceϕ,

ϕis satisfiable ⇔ E(ϕ)is satisfiable. proof.(⇒)

Letϕ ≡ ∀x₁...∀x_nϕ₀(x₁, ...,x_n)is satisfiable. If _{M |= ∀x1}...∀x_nϕ0^(x1, ...,x_n),

M |= ϕ0^(t1^{, ...,t}n⁾for all variable-freeV_ϕ-termt_i. This is that _{M |= E(ϕ)}, soE(ϕ)is satisfiable.

To prove the converse, we assert following Lemma.

Theorem.1

For any equality-free SNF sentenceϕ,

ϕis satisfiable ⇔ E(ϕ)is satisfiable. proof.(⇒)

Letϕ ≡ ∀x₁...∀x_nϕ₀(x₁, ...,x_n)is satisfiable. If _{M |= ∀x1}...∀x_nϕ0^(x1, ...,x_n),

M |= ϕ0^(t1^{, ...,t}n⁾for all variable-freeV_ϕ-termt_i. This is that _{M |= E(ϕ)}, soE(ϕ)is satisfiable.

To prove the converse, we assert following Lemma.

Theorem.1

For any equality-free SNF sentenceϕ,

ϕis satisfiable ⇔ E(ϕ)is satisfiable. proof.(⇒)

Letϕ ≡ ∀x₁...∀x_nϕ₀(x₁, ...,x_n)is satisfiable. If _{M |= ∀x1}...∀x_nϕ0^(x1, ...,x_n),

M |= ϕ0^(t1^{, ...,t}n⁾for all variable-freeV_ϕ-termt_i. This is that _{M |= E(ϕ)}, soE(ϕ)is satisfiable.

To prove the converse, we assert following Lemma.

Lemma.1

Let_Γbe a set of equality-free SNF sentence. Then,

Γis satisfiable _{⇔ Γ}has a Herbrand model. outline of proof.

If_Γhas a Herbrand model,_Γis satisfiable. Conversely, suppose_Γis satisfiable. LetV_Γbe the Herbrand vocabulary for_Γ.

LetN be aV_Γ-structure that models_Γand M^′ be a Herbrand V_Γ-structure.

Then, we can make a HerbrandV_Γ-structure M fromN and M^′, that models_Γ.

The universe of Mis same to M^′. Minterprets constants and functions the same way as M^′and relations the same way as N.

Lemma.1

Let_Γbe a set of equality-free SNF sentence. Then,

Γis satisfiable _{⇔ Γ}has a Herbrand model. outline of proof.

If_Γhas a Herbrand model,_Γis satisfiable. Conversely, suppose_Γis satisfiable. LetV_Γbe the Herbrand vocabulary for_Γ.

LetN be aV_Γ-structure that models_Γand M^′ be a Herbrand V_Γ-structure.

Then, we can make a HerbrandV_Γ-structure M fromN and M^′, that models_Γ.

The universe of Mis same to M^′. Minterprets constants and functions the same way as M^′and relations the same way as N.

Theorem.1

For any equality-free SNF sentenceϕ,

ϕis satisfiable ⇔ E(ϕ)is satisfiable. proof.(⇐)

Suppose E(ϕ)is satisfiable andϕ ≡ ∀x₁...∀x_nϕ0^(x1, ...,x_n). By Lemma.1, E(ϕ)has a Herbrand model M.

Since the Herbrand vocabulary forE(ϕ)is the same as the Herbrand vocabulary forϕ, the universe ofM isH(ϕ). For eacht₁, ...,t_nin H(ϕ),

M |= ϕ0^(t1^{, ...,t}n⁾since this sentence is inE(ϕ). That is, _{M |= ϕ}.

ϕis satisfiable.

Resolution

Resolution is a system of formal proof that involves a minimal number of rule.

It is made by J.A.Robinson(Reference.3) for the purpose of providing a method of proof that can be done by a computer. Resolution can be used to determine whether or not any given sentence is satisfiable.

First, we define resolution principle for propositional logic. Definition.

Clauseis a disjunction of literals. From now, I write each clause as a set. LetC₁andC₂ be two clauses.

Suppose that A ∈ C1 and¬A ∈ C₂ for some atomic formulaA. Then the clause_{R = (C1}− {A}) ∪ (C₂− {¬A})is aresolventofC₁ andC₂.

Example.

{A₁,A₂, ¬A₂,A₄}is a resolvent of{A₁, ¬A₂,A₃}and{A₂, ¬A₃,A₄}. {A₁,A₃, ¬A₃,A₄}is also a resolvent of{A₁, ¬A₂,A₃}and

{A₂, ¬A₃,A₄}.

Definition.

LetF be a set of formulas in conjunctive normal form (CNF). Res (F) _{:= {R | R}is resolvent of two clauses inF}

Res⁰(F) := {C | C is a clause in F} Resⁿ_{(F) := Res}ⁿ⁻¹(F) ∪ Res(Resⁿ⁻¹(F)) Res^∗_{(F) :=} ^∪

n∈N

Resⁿ(F)

Fact.3

LetF be a set of CNF formula. Then

F is unsatifiable ⇔ ∅ ∈ Res^∗(F).

Definition.

LetF be a set of formulas in conjunctive normal form (CNF). Res (F) _{:= {R | R}is resolvent of two clauses inF}

Res⁰(F) := {C | C is a clause in F} Resⁿ_{(F) := Res}ⁿ⁻¹(F) ∪ Res(Resⁿ⁻¹(F)) Res^∗_{(F) :=} ^∪

n∈N

Resⁿ(F)

Fact.3

LetF be a set of CNF formula. Then

F is unsatifiable ⇔ ∅ ∈ Res^∗(F).

Next, we define resolution principle for first-order logic. Definition.

For any SNF sentenceϕ,

clauseinϕis a clause in CNF formulaϕ₀whereϕis

∀x1...∀xnϕ0.

Let_{L = {L1}, ...,L_n}is a clause (set of literals).

L_isunifiableif there exist substitution subsuch that^Lsub contains only one literal.

subis themost general unifier for^L

if it unifies^Land subsub^′ _{= sub}^′ for any other unifier sub^′for L_.

Example.

LetL = {P( f (x), y), P( f (a), z)}^.

( It represent∀x∀y∀z(P( f (x), y) ∨ P( f (a), z)). ) Let sub1= (x/a, y/z)^.

Then^Lsub₁= {P( f (a), z)}^{, so L}is unifiable. Moreover, sub₁is the most general unifier for^L.

For instance, sub₂= (x/a, y/a, z/a)is also unifier for^L, whereas sub₁sub_{2= sub2}.

Fact.4

We can exhibit an algorithm that, given^Las input, outputs

{ NOT UNIFIABLE if^Lis not unifiable the most general unifier for^L if^Lis unifiable.

Example.

LetL = {P( f (x), y), P( f (a), z)}^.

( It represent∀x∀y∀z(P( f (x), y) ∨ P( f (a), z)). ) Let sub1= (x/a, y/z)^.

Then^Lsub₁= {P( f (a), z)}^{, so L}is unifiable. Moreover, sub₁is the most general unifier for^L.

For instance, sub₂= (x/a, y/a, z/a)is also unifier for^L, whereas sub₁sub_{2= sub2}.

Fact.4

We can exhibit an algorithm that, given^Las input, outputs

{ NOT UNIFIABLE if^Lis not unifiable the most general unifier for^L if^Lis unifiable.

Definition.

LetC₁andC₂ be two clauses in first-order formula.

Lets₁ and s₂ be any substitutions such thatC₁s₁ andC₂s₂have no variables in common.

Let{L₁, ...,L_m} ⊂ C₁s₁and{L^′₁, ...,L^′_n} ⊂ C₂s₂be such that L = { ¯^L1^{, ..., ¯L}m^,L′₁^{, ...,L′}_n^}is unifiable, where_{L = ¬L}^¯ or¬ ¯_{L = L}. Let subbe the most general unifier for^L.

Then_{R = [(C1}s₁− {L₁, ...,L_m}) ∪ (C₂s₂− {L₁^′, ...,L^′_n})]subis a resolventofC₁andC₂.

Fact.5 (Soundness)

Ris a resolvent ofC1andC2 ⇒ Ris a consequence ofC1 andC2

Definition.

LetC₁andC₂ be two clauses in first-order formula.

Lets₁ and s₂ be any substitutions such thatC₁s₁ andC₂s₂have no variables in common.

Let{L₁, ...,L_m} ⊂ C₁s₁and{L^′₁, ...,L^′_n} ⊂ C₂s₂be such that L = { ¯^L1^{, ..., ¯L}m^,L′₁^{, ...,L′}_n^}is unifiable, where_{L = ¬L}^¯ or¬ ¯_{L = L}. Let subbe the most general unifier for^L.

Then_{R = [(C1}s₁− {L₁, ...,L_m}) ∪ (C₂s₂− {L₁^′, ...,L^′_n})]subis a resolventofC₁andC₂.

Fact.5 (Soundness)

Ris a resolvent ofC1andC2 ⇒ Ris a consequence ofC1 andC2

Example.

LetC₁= {Q(x, y), P( f (x), y)}^and

C2 = {R(x, c), ¬P( f (c), x), ¬P( f (y), h(z))}^. We find a resolvent ofC₁andC₂.

Let s₁= (x/u, y/v)^.

ThenC₁s₁ = {Q(u, v), P( f (u), v)}, which has no variable in common withC2.

LetL = {¬P( f (u), v), ¬P( f (c), x), ¬P( f (y), h(z))}^.

Then^Lis unifiable andsub = (u/c, y/c, v/h(z), x/h(z))is the most general unifier.

We conclude thatC₁ andC₂have resolvent

R = ^[(C1^s1− {P( f (u), v)}) ∪ (C₂− {¬P( f (c), x), ¬P( f (y), h(z))})] sub

= {Q(u, v), R(x, c)}sub

= {Q(c, h(z)), R(h(z), c)}.

Example.

Next, we check the soundness.

C₁ represents∀x∀y (Q(x, y) ∨ P( f (x), y)), and

C₂ represents∀x∀y∀z (R(x, c) ∨ ¬P( f (c), x) ∨ ¬P( f (y), h(z))). SupposeC1 andC2hold in some structure.

Then they hold no matter what we plog in for the variables. In particular,

C1s1sub ≈ ∀z (Q(c, h(z)) ∨ P( f (c), h(z))), and C₂sub ^≈∀z (R(h(z), c) ∨ ¬P( f (c), h(z))) both hold. ThenR ≈ ∀z (Q(c, h(z)), R(h(z), c)) holds.

Definition.

Letϕbe a SNF sentence.

Res (ϕ) _{:= {R | R}is resolvent of two clauses inϕ} Res⁰(ϕ) := {C | C is a clause inϕ}

Resⁿ_{(ϕ) := Res}ⁿ⁻¹(ϕ) ∪ Res(Resⁿ⁻¹(ϕ)) Res^∗_{(ϕ) :=} ^∪

n∈N

Resⁿ(ϕ)

Theorem.2

For any equality-free SNF sentenceϕ,

ϕis unsatisfiable⇔ ∅ ∈ Res^∗(ϕ). proof.(⇐)

Let∅ ∈ Res^∗(ϕ).

Then there existn > 0s.t. ∅ ∈ Resⁿ(ϕ).

Then there exist an atomic formula Land sets of atomic formulas L_{1, L2 ∈ Res}ⁿ⁻¹_{(ϕ)and a}sub, such that^L¯_{1sub = L2sub = {L}}. Suppose that _{M |= ϕ},M |= ¯L ∨ Lby the soundness of resolution. ButL ∨ L^¯ is contradiction.

Soϕis unsatisfiable.

To prove the converse, we assert following Lemma and Corollary.

Theorem.2

For any equality-free SNF sentenceϕ,

ϕis unsatisfiable⇔ ∅ ∈ Res^∗(ϕ). proof.(⇐)

Let∅ ∈ Res^∗(ϕ).

Then there existn > 0s.t. ∅ ∈ Resⁿ(ϕ).

Then there exist an atomic formula Land sets of atomic formulas L_{1, L2 ∈ Res}ⁿ⁻¹_{(ϕ)and a}sub, such that^L¯_{1sub = L2sub = {L}}. Suppose that _{M |= ϕ},M |= ¯L ∨ Lby the soundness of resolution. ButL ∨ L^¯ is contradiction.

Soϕis unsatisfiable.

To prove the converse, we assert following Lemma and Corollary.

Theorem.2

For any equality-free SNF sentenceϕ,

ϕis unsatisfiable⇔ ∅ ∈ Res^∗(ϕ). proof.(⇐)

Let∅ ∈ Res^∗(ϕ).

Then there existn > 0s.t. ∅ ∈ Resⁿ(ϕ).

Then there exist an atomic formula Land sets of atomic formulas L_{1, L2 ∈ Res}ⁿ⁻¹_{(ϕ)and a}sub, such that^L¯_{1sub = L2sub = {L}}. Suppose that _{M |= ϕ},M |= ¯L ∨ Lby the soundness of resolution. ButL ∨ L^¯ is contradiction.

Soϕis unsatisfiable.

To prove the converse, we assert following Lemma and Corollary.

Lemma. (Lifting lemma) Letϕbe a SNF sentence.

IfR^′ ∈ Res(E(ϕ)), then there existR ∈ Res(ϕ)such thatRsub^′ _{= R}^′ for some sub^′.

outline of proof.

LetC₁^′ andC₂^′ inE(ϕ)be such thatC₁s₁sub_{1= C}^′₁andC₂sub_{2 = C}^′₂. LetR^′be a resolvent ofC^′₁andC^′₂ (in propositional logic sence). Then there exist some literal L ∈ C₁^′ such thatL ∈ C^{¯ ′}₂and

R^′ _{= (C1}^′ − {L}) ∪ (C₂^′ − { ¯L}). sub^′ _{:= sub1}sub₂.

ThenC₁s₁sub^′ _{= C1}s₁sub_{1 = C1}^′ andC₂sub^′ _{= C2}sub_{2 = C2}^′.

Let^L₁ ⊂ C₁s₁be s.t. ^L₁sub^′ _{= {L}}and^L₂⊂ C₂be s.t.^L₂sub^′ _{= { ¯L}}. L_{:= ¯}L_{1∪ L2}is unifiable since^Lsub^′_{= { ¯L}}.

Let subbe the most general unifier for^L.

R := [(C1^s1^{− L}1^{) ∪ (C}2^{− L}2^)]subis a resolvent ofC₁ andC₂. Then,Rsub^′ _{= R}^′.

Lemma. (Lifting lemma) Letϕbe a SNF sentence.

IfR^′ ∈ Res(E(ϕ)), then there existR ∈ Res(ϕ)such thatRsub^′ _{= R}^′ for some sub^′.

outline of proof.

LetC₁^′ andC₂^′ inE(ϕ)be such thatC₁s₁sub_{1= C}^′₁andC₂sub_{2 = C}^′₂. LetR^′be a resolvent ofC^′₁andC^′₂ (in propositional logic sence). Then there exist some literal L ∈ C₁^′ such thatL ∈ C^{¯ ′}₂and

R^′ _{= (C1}^′ − {L}) ∪ (C₂^′ − { ¯L}). sub^′ _{:= sub1}sub₂.

ThenC₁s₁sub^′ _{= C1}s₁sub_{1 = C1}^′ andC₂sub^′ _{= C2}sub_{2 = C2}^′.

Let^L₁ ⊂ C₁s₁be s.t. ^L₁sub^′ _{= {L}}and^L₂⊂ C₂be s.t.^L₂sub^′ _{= { ¯L}}. L_{:= ¯}L_{1∪ L2}is unifiable since^Lsub^′_{= { ¯L}}.

Let subbe the most general unifier for^L.

R := [(C1^s1^{− L}1^{) ∪ (C}2^{− L}2^)]subis a resolvent ofC₁ andC₂. Then,Rsub^′ _{= R}^′.

Corollary.

Letϕbe a SNF sentence.

IfC^′ ∈ Res^∗(E(ϕ)), then there existC ∈ Res^∗(ϕ)and asub^′ such thatC sub^′_{= C}^′.

proof.

IfC^′∈ Res^∗(E(ϕ)),C^′∈ Resⁿ(E(ϕ))for somen. We prove by induction onn.

If_{n = 0}, thenC^′∈ E(ϕ).

By definition ofE(ϕ),C^′is obtained byC ∈ ϕ ⊂ Res^∗(ϕ)via substitution. For induction step, suppose the case ofmis satisfied.

Letϕ ⊂˜ Res^∗(ϕ)be s.t. Res^m(E(ϕ))comes fromϕ˜ via substitution. Then,Res^m(E(ϕ)) ⊂ E( ˜ϕ).

IfC^′∈ Res^m+1(E(ϕ)), thenC^′ ∈ Res (E( ˜ϕ))since

Res^m(E(ϕ)) ⊂ E( ˜ϕ) ⊂ Res (E( ˜ϕ))andRes (Res^m(E(ϕ))) ⊂ Res (E( ˜ϕ)). By Lifting lemma, there existC ∈ Res( ˜ϕ)s.t.C sub^′ _{= C}^′for somesub^′. Sinceϕ ⊂˜ Res^∗(E(ϕ)),C ∈ Res^∗(ϕ).

Corollary.

Letϕbe a SNF sentence.

IfC^′ ∈ Res^∗(E(ϕ)), then there existC ∈ Res^∗(ϕ)and asub^′ such thatC sub^′_{= C}^′.

proof.

IfC^′∈ Res^∗(E(ϕ)),C^′∈ Resⁿ(E(ϕ))for somen. We prove by induction onn.

If_{n = 0}, thenC^′∈ E(ϕ).

By definition ofE(ϕ),C^′is obtained byC ∈ ϕ ⊂ Res^∗(ϕ)via substitution. For induction step, suppose the case ofmis satisfied.

Letϕ ⊂˜ Res^∗(ϕ)be s.t. Res^m(E(ϕ))comes fromϕ˜ via substitution. Then,Res^m(E(ϕ)) ⊂ E( ˜ϕ).

IfC^′∈ Res^m+1(E(ϕ)), thenC^′ ∈ Res (E( ˜ϕ))since

Res^m(E(ϕ)) ⊂ E( ˜ϕ) ⊂ Res (E( ˜ϕ))andRes (Res^m(E(ϕ))) ⊂ Res (E( ˜ϕ)). By Lifting lemma, there existC ∈ Res( ˜ϕ)s.t.C sub^′ _{= C}^′for somesub^′. Sinceϕ ⊂˜ Res^∗(E(ϕ)),C ∈ Res^∗(ϕ).

Theorem.2

For any equality-free SNF sentenceϕ,

ϕis unsatisfiable⇔ ∅ ∈ Res^∗(ϕ). proof.(^⇒)

By corollary, in particular, if∅ ∈ Res^∗(E(ϕ)), there exist some C ∈ Res^∗(ϕ)s.t. C sub^′ _{= ∅}for somesub^′.

But this is only possible if_{C = ∅}. So if∅ ∈ Res^∗(E(ϕ)), then∅ ∈ Res^∗(ϕ).

By Theorem.1, Fact.3 and above, the proof is complete. [Theorem.1] For any equality-free SNF sentenceϕ,

ϕis satisfiable ⇔ E(ϕ)is satisfiable. [Fact.3] LetF be a set of CNF formula.

Then,Fis unsatifiable ⇔ ∅ ∈ Res^∗(F).

By Fact.1, Fact.2 and Theorem.2, we can conclude as follows.

Conclusion.

For any first-order sentenceϕ,

ϕis unsatisfiable ⇔ ∅ ∈ Res^∗((ϕ^S)_E⁾.

[Fact.1] For any formulaϕof first-order logic, ϕis satisfiable ⇔ ϕ^S is satisfiable. [Fact.2] For any SNF sentenceϕ,

ϕis satisfiable ⇔ ϕE is satisfiable. [Theorem.2] For any equality-free SNF sentenceϕ,

ϕis unsatisfiable ⇔ ∅ ∈ Res^∗(ϕ).

Reference

1 SHAWN HEDMAN, A First Course in Logic: An introduction to model theory, proof theory, computability, and complexity, Oxford University Press(2004).

2 岩波 数学辞典 第四版_,日本数学会編集_,岩波書店_(2007).

3 J.A.Robinson, A Machine-oriented Logic Based on the Resolution Principle, J.Association for Computing Machinery,12(1965),23-41.

Thank you for your attention !