1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
s/<g>term<\/g>/<a href="glossary.html#term">term<\/a>/
s/<g>terms<\/g>/<a href="glossary.html#term">terms<\/a>/
s/<g>atomic formula<\/g>/<a href="glossary.html#atomic formula">atomic formula<\/a>/
s/<g>formula<\/g>/<a href="glossary.html#formula">formula<\/a>/
s/<g>free variable<\/g>/<a href="glossary.html#quantifiers">free variable<\/a>/
s/<g>open formula<\/g>/<a href="glossary.html#quantifiers">open formula<\/a>/
s/<g>closed formula<\/g>/<a href="glossary.html#quantifiers">closed formula<\/a>/
s/<g>closed formulas<\/g>/<a href="glossary.html#quantifiers">closed formulas<\/a>/
s/<g>literal<\/g>/<a href="glossary.html#literal">literal<\/a>/
s/<g>clause<\/g>/<a href="glossary.html#clause">clause<\/a>/
s/<g>clauses<\/g>/<a href="glossary.html#clause">clauses<\/a>/
s/<g>interpretation<\/g>/<a href="glossary.html#interpretation">interpretation<\/a>/
s/<g>unit clause<\/g>/<a href="glossary.html#unit-clause">unit clause<\/a>/
s/<g>positive clause<\/g>/<a href="glossary.html#clause-signs">positive clause<\/a>/
s/<g>negative clause<\/g>/<a href="glossary.html#clause-signs">negative clause<\/a>/
s/<g>mixed clause<\/g>/<a href="glossary.html#clause-signs">mixed clause<\/a>/
s/<g>non-Horn<\/g>/<a href="glossary.html#horn">non-Horn<\/a>/
s/<g>non-Horn clause<\/g>/<a href="glossary.html#horn">non-Horn clause<\/a>/
s/<g>non-Horn clauses<\/g>/<a href="glossary.html#horn">non-Horn clauses<\/a>/
s/<g>Horn<\/g>/<a href="glossary.html#horn">Horn<\/a>/
s/<g>Horn clause<\/g>/<a href="glossary.html#horn">Horn clause<\/a>/
s/<g>Horn set<\/g>/<a href="glossary.html#horn">Horn set<\/a>/
s/<g>Horn clauses<\/g>/<a href="glossary.html#horn">Horn clauses<\/a>/
s/<g>Horn sets<\/g>/<a href="glossary.html#horn">Horn sets<\/a>/
s/<g>definite clause<\/g>/<a href="glossary.html#definite-clause">definite clause<\/a>/
s/<g>negation normal form<\/g>/<a href="glossary.html#NNF">negation normal form<\/a>/
s/<g>NNF<\/g>/<a href="glossary.html#NNF">NNF<\/a>/
s/<g>conjunctive normal form<\/g>/<a href="glossary.html#CNF">conjunctive normal form<\/a>/
s/<g>CNF<\/g>/<a href="glossary.html#CNF">CNF<\/a>/
s/<g>Skolemization<\/g>/<a href="glossary.html#skolemization">Skolemization<\/a>/
s/<g>skolemization<\/g>/<a href="glossary.html#skolemization">skolemization<\/a>/
s/<g>Skolem constant<\/g>/<a href="glossary.html#skolemization">Skolem constant<\/a>/
s/<g>Skolem function<\/g>/<a href="glossary.html#skolemization">Skolem function<\/a>/
s/<g>Skolem<\/g>/<a href="glossary.html#skolemization">Skolem<\/a>/
s/<g>clause normal form<\/g>/<a href="glossary.html#clausification">clause normal form<\/a>/
s/<g>clausification<\/g>/<a href="glossary.html#clausification">clausification<\/a>/
s/<g>clausify<\/g>/<a href="glossary.html#clausification">clausify<\/a>/
s/<g>kbo<\/g>/<a href="glossary.html#KBO">kbo<\/a>/
s/<g>KBO<\/g>/<a href="glossary.html#KBO">KBO<\/a>/
s/<g>LPO<\/g>/<a href="glossary.html#LPO">LPO<\/a>/
s/<g>lpo<\/g>/<a href="glossary.html#LPO">lpo<\/a>/
s/<g>RPO<\/g>/<a href="glossary.html#RPO">RPO<\/a>/
s/<g>rpo<\/g>/<a href="glossary.html#RPO">rpo<\/a>/
s/<g>maximal<\/g>/<a href="glossary.html#maximal">maximal<\/a>/
s/<g>maximal literal<\/g>/<a href="glossary.html#maximal">maximal literal<\/a>/
s/<g>maximal literals<\/g>/<a href="glossary.html#maximal">maximal literals<\/a>/
s/<g>completeness<\/g>/<a href="glossary.html#completeness">completeness<\/a>/
s/<g>binary resolution<\/g>/<a href="glossary.html#Binary Resolution">binary resolution<\/a>/
s/<g>resolution<\/g>/<a href="glossary.html#Binary Resolution">resolution<\/a>/
s/<g>positive resolution<\/g>/<a href="glossary.html#Binary Resolution">positive resolution<\/a>/
s/<g>negative resolution<\/g>/<a href="glossary.html#Binary Resolution">negative resolution<\/a>/
s/<g>positive binary resolution<\/g>/<a href="glossary.html#Binary Resolution">positive binary resolution<\/a>/
s/<g>negative binary resolution<\/g>/<a href="glossary.html#Binary Resolution">negative binary resolution<\/a>/
s/<g>ordered resolution<\/g>/<a href="glossary.html#ordered-inf">ordered resolution<\/a>/
s/<g>ordered paramodulation<\/g>/<a href="glossary.html#ordered-inf">ordered paramodulation<\/a>/
s/<g>literal selection<\/g>/<a href="glossary.html#ordered-inf">literal selection<\/a>/
s/<g>factoring<\/g>/<a href="glossary.html#factoring">factoring<\/a>/
s/<g>binary factoring<\/g>/<a href="glossary.html#factoring">binary factoring<\/a>/
s/<g>factor<\/g>/<a href="glossary.html#factoring">factor<\/a>/
s/<g>factorization<\/g>/<a href="glossary.html#factoring">factorization<\/a>/
s/<g>hyperresolution<\/g>/<a href="glossary.html#hyperresolution">hyperresolution<\/a>/
s/<g>negative hyperresolution<\/g>/<a href="glossary.html#hyperresolution">negative hyperresolution<\/a>/
s/<g>nucleus<\/g>/<a href="glossary.html#hyperresolution">nucleus<\/a>/
s/<g>satellite<\/g>/<a href="glossary.html#hyperresolution">satellite<\/a>/
s/<g>UR-resolution<\/g>/<a href="glossary.html#UR-resolution">UR-resolution<\/a>/
s/<g>positive UR-resolution<\/g>/<a href="glossary.html#UR-resolution">positive UR-resolution<\/a>/
s/<g>negative UR-resolution<\/g>/<a href="glossary.html#UR-resolution">negative UR-resolution<\/a>/
s/<g>unit-resulting resolution<\/g>/<a href="glossary.html#UR-resolution">unit-resulting resolution<\/a>/
s/<g>paramodulation<\/g>/<a href="glossary.html#from-into">paramodulation<\/a>/
s/<g>from parent<\/g>/<a href="glossary.html#from-into">from parent<\/a>/
s/<g>from clause<\/g>/<a href="glossary.html#from-into">from clause<\/a>/
s/<g>from literal<\/g>/<a href="glossary.html#from-into">from literal<\/a>/
s/<g>into term<\/g>/<a href="glossary.html#from-into">into term<\/a>/
s/<g>into parent<\/g>/<a href="glossary.html#from-into">into parent<\/a>/
s/<g>into clause<\/g>/<a href="glossary.html#from-into">into clause<\/a>/
s/<g>into literal<\/g>/<a href="glossary.html#from-into">into literal<\/a>/
s/<g>into term<\/g>/<a href="glossary.html#from-into">into term<\/a>/
s/<g>superposition<\/g>/<a href="glossary.html#from-into">superposition<\/a>/
s/<g>positive paramodulation<\/g>/<a href="glossary.html#positive-paramodulation">positive paramodulation<\/a>/
s/<g>demodulation<\/g>/<a href="glossary.html#demodulation">demodulation<\/a>/
s/<g>demodulator<\/g>/<a href="glossary.html#demodulation">demodulator<\/a>/
s/<g>rewriting<\/g>/<a href="glossary.html#demodulation">rewriting<\/a>/
s/<g>back demodulation<\/g>/<a href="glossary.html#demodulation">back demodulation<\/a>/
s/<g>demodulator<\/g>/<a href="glossary.html#demodulation">demodulator<\/a>/
s/<g>unit deletion<\/g>/<a href="glossary.html#unit-deletion">unit deletion<\/a>/
s/<g>back unit deletion<\/g>/<a href="glossary.html#unit-deletion">back unit deletion<\/a>/
s/<g>subsume<\/g>/<a href="glossary.html#subsumption">subsume<\/a>/
s/<g>subsumption<\/g>/<a href="glossary.html#subsumption">subsumption<\/a>/
s/<g>back subsumption<\/g>/<a href="glossary.html#subsumption">back subsumption<\/a>/
s/<g>forward subsumption<\/g>/<a href="glossary.html#subsumption">forward subsumption<\/a>/
s/<g>unit conflict<\/g>/<a href="glossary.html#conflict">unit conflict<\/a>/
s/<g>given clause<\/g>/<a href="glossary.html#given-clause">given clause<\/a>/
s/<g>given clause algorithm<\/g>/<a href="glossary.html#given-clause">given clause algorithm<\/a>/
s/<g>given clause loop <\/g>/<a href="glossary.html#given-clause">given clause loop <\/a>/
s/<g>given clauses<\/g>/<a href="glossary.html#given-clause">given clauses<\/a>/
s/<g>assumptions<\/g>/<a href="glossary.html#sos-usable">assumptions<\/a>/
s/<g>assumptions list<\/g>/<a href="glossary.html#sos-usable">assumptions list<\/a>/
s/<g>sos<\/g>/<a href="glossary.html#sos-usable">sos<\/a>/
s/<g>sos list<\/g>/<a href="glossary.html#sos-usable">sos list<\/a>/
s/<g>usable<\/g>/<a href="glossary.html#sos-usable">usable<\/a>/
s/<g>usable list<\/g>/<a href="glossary.html#sos-usable">usable list<\/a>/
s/<g>goal<\/g>/<a href="glossary.html#goals">goal<\/a>/
s/<g>goals list<\/g>/<a href="glossary.html#goals">goals list<\/a>/
s/<g>goals<\/g>/<a href="glossary.html#goals">goals<\/a>/
s/<g>hint<\/g>/<a href="glossary.html#hints">hint<\/a>/
s/<g>hints list<\/g>/<a href="glossary.html#hints">hints list<\/a>/
s/<g>hints<\/g>/<a href="glossary.html#hints">hints<\/a>/
s/<g>initial clause<\/g>/<a href="glossary.html#initial">initial clause<\/a>/
s/<g>input clause<\/g>/<a href="glossary.html#initial">input clause<\/a>/
s/<g>denial<\/g>/<a href="glossary.html#denials">denial<\/a>/
s/<g>denials list<\/g>/<a href="glossary.html#denials">denials list<\/a>/
s/<g>denials<\/g>/<a href="glossary.html#denials">denials<\/a>/
s/<g>fof reduction<\/g>/<a href="glossary.html#fof-reduction">fof reduction<\/a>/
s/<g>lex-dependent demodulator<\/g>/<a href="glossary.html#lex-dep">lex-dependent demodulator<\/a>/
s/<g>lex-dependent demodulation<\/g>/<a href="glossary.html#lex-dep">lex-dependent demodulation<\/a>/
s/<g>depth of the term<\/g>/<a href="glossary.html#depth-C">depth of the term<\/a>/
s/<g>depth of the atom<\/g>/<a href="glossary.html#depth-C">depth of the atom<\/a>/
s/<g>depth of the literal<\/g>/<a href="glossary.html#depth-C">depth of the literal<\/a>/
s/<g>depth of the clause<\/g>/<a href="glossary.html#depth-C">depth of the clause<\/a>/
s/<g>depth(C)<\/g>/<a href="glossary.html#depth-C">depth(C)<\/a>/
s/<g>relational definition<\/g>/<a href="glossary.html#relational-def">relational definition<\/a>/
s/<g>equational definition<\/g>/<a href="glossary.html#equational-def">equational definition<\/a>/
|
