/usr/share/doc/prover9-doc/html/glossary.html is in prover9-doc 0.0.200902a-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Glossary</title>
<link rel="stylesheet" href="manual.css">
</head>
<body>
<hr>
<table width="100%">
<tr>
<colgroup>
<col width="33%">
<col width="34%">
<col width="33%">
</colgroup>
<td align="left"><i>Prover9 Manual</i>
<td align="center"><img src="prover9-5a-256t.gif">
<td align="right"><i>Version 2009-02A</i>
</table>
<hr>
<!-- Main content -->
<h1>Glossary</h1>
<i>Under construction. (Send suggestions of terms to include.)</i>
<hr>
<hr>
<h2>Terms, Clauses, Formulas, Interpretations</h2>
These definitions apply to first-order unsorted logic.
See a book on first-order logic for more formal definitions
of these concepts.
<hr>
<!-- start def term -->
<!-- start def terms -->
<a name="term">
<i>Term</i>
<blockquote>
A recursive definition of first-order unsorted <i class="g">terms</i>.
<ul>
<li>A variable is a term,
<li>a constant is a term, and
<li>an <i>n</i>-ary function symbol applied to <i>n</i> terms is a term.
</ul>
</blockquote>
<hr>
<!-- start def atomic formula -->
<a name="atomic formula">
<i>Atomic Formula</i>
<blockquote>
An <i>n</i>-ary predicate symbol applied to <i>n</i> terms
is an <i class="g">atomic formula</i>.
</blockquote>
<hr>
<!-- start def formula -->
<a name="formula">
<i>Formula</i>
<blockquote>
<ul>
<li>An atomic formula is a formula,
<li>if <tt>F</tt> and <tt>G</tt> are formulas, then the following are formulas.
<ul>
<li><tt>(-F)</tt>
<li><tt>(F | G)</tt>
<li><tt>(F & G)</tt>
<li><tt>(F -> G)</tt>
<li><tt>(F <-> G)</tt>
</ul>
<li>if <tt>F</tt> is a formula and <tt>x</tt> is a variable, then the
following are formulas.
<ul>
<li><tt>(all x F)</tt>
<li><tt>(exists x F)</tt>
</ul>
</ul>
When writing formulas for Prover9, many of the parentheses can be
omitted; see the page <a href="syntax.html">Clauses and Formulas</a>
tor the parsing rules.
</blockquote>
<hr>
<!-- start def free variable -->
<!-- start def open formula -->
<!-- start def closed formula -->
<!-- start def closed formulas -->
<a name="quantifiers">
<i>Free Variables</i>
<blockquote>
A <i class="g">free variable</i> is a variable not bound by any quantifier.
A <i class="g">closed formula</i> has no free variables.
An <i class="g">open formula</i> has at least one free variable.
<p>
Prover9's default rule for distinguishing free variables
from constants is that free varaibles start with (lower case)
'<tt>u</tt>' through '<tt>z</tt>'.
</blockquote>
<hr>
<!-- start def literal -->
<a name="literal">
<i>Literal</i>
<blockquote>
A <i class="g">literal</i> is either an
<a href="glossary.html#atomic formula">atomic formula</a>
or the negation of an atomic formula.
</blockquote>
<hr>
<!-- start def clause -->
<!-- start def clauses -->
<a name="clause">
<i>Clause</i>
<blockquote>
A <i class="g">clause</i> is a formula consisting of a disjunction of literals.
All variables in a clause are
assumed to be universally quantified.
</blockquote>
<hr>
<!-- start def interpretation -->
<a name="interpretation">
<i>Interpretation</i>
<blockquote>
An <i class="g">interpretation</i> of a first-order language consists of
<ul>
<li> of a set of objects called the <i class="g">domain</i>,
<li> an <i>n</i>-ary function over the domain into the domain for
each <i>n</i>-ary function symbol in the language,
<li> an <i>n</i>-ary relation over the domain for
each <i>n</i>-ary predicate symbol in the language.
</ul>
</blockquote>
Given an interpretation, each term in the language
evaluates to a member of the domain, and
each clause or
closed formula in the language evaluates to TRUE or to FALSE.
<hr>
<hr>
<h2>Types of Clause</h2>
<hr>
<!-- start def unit clause -->
<a name="unit-clause">
<i>Unit Clause</i>
<blockquote>
A <i class="g">unit clause</i> has exactly one literal.
</blockquote>
<hr>
<!-- start def positive clause -->
<!-- start def negative clause -->
<!-- start def mixed clause -->
<a name="clause-signs">
<i>Positive Clause, Negative Clause, Mixed Clause</i>
<blockquote>
A <i class="g">positive clause</i> has no negative literals.
A <i class="g">negative clause</i> has no positive literals.
Note that the empty clause is both positive and negative.
A <i class="g">mixed clause</i> has at least one literal of each sign.
</blockquote>
<hr>
<!-- start def non-Horn -->
<!-- start def non-Horn clause -->
<!-- start def non-Horn clauses -->
<!-- start def Horn -->
<!-- start def Horn clause -->
<!-- start def Horn set -->
<!-- start def Horn clauses -->
<!-- start def Horn sets -->
<a name="horn">
<i>Horn Clause, Horn Set</i>
<blockquote>
A <i class="g">Horn clause</i> has at most one positive literal.
A Horn set is a set of Horn clauses.
</blockquote>
<hr>
<!-- start def definite clause -->
<a name="definite-clause">
<i>Definite Clause</i>
<blockquote>
A <i class="g">definite clause</i> has exactly one positive literal.
</blockquote>
<hr>
<hr>
<h2>Logic Transformations</h2>
<hr>
<!-- start def negation normal form -->
<!-- start def NNF -->
<a name="NNF">
<i>Negation Normal Form (NNF)</i>
<blockquote>
A formula is in <i class="g">negation normal form</i>
if the only logic connectives are
negation, conjunction, disjunction, quantification (universal or existential),
and if all negation operations are applied directly to atomic formulas.
</blockquote>
<hr>
<!-- start def conjunctive normal form -->
<!-- start def CNF -->
<a name="CNF">
<i>Conjunctive Normal Form (CNF)</i>
<blockquote>
This definition applies to quantifier-free formulas.
<p>
A formula is in <i class="g">conjunctive normal form</i>
if (1) the only logic connectives
are negation, conjunction, and disjunction,
(2) no negation is applied to a conjunction or a disjunction,
and (3) no disjunction is applied to a conjunction.
<p>
Alternate definition: A formula is in CNF if it is a clause or a
conjunction of clauses.
</blockquote>
<hr>
<!-- start def Skolemization -->
<!-- start def skolemization -->
<!-- start def Skolem constant -->
<!-- start def Skolem function -->
<!-- start def Skolem -->
<a name="skolemization">
<i>Skolemization</i>
<blockquote>
</i>Skolemization</i> is the process of replacing
existentially quantified variables
in a formula with new constants (called <i class="g">Skolem constants</i>) or
functions (called <i class="g">Skolem functions</i>). If an existential
quantifier is in the scope of some universal quantifiers, the
new symbol is a function of the corresponding universally quantified
variables.
The result of Skolemization is not, strictly speaking, equivalent to
the original formula, because new symbols may have been introduced,
but the result is inconsistent iff the the original formula is
inconsistent.
</blockquote>
<hr>
<!-- start def clause normal form -->
<!-- start def clausification -->
<!-- start def clausify -->
<a name="clausification">
<i>Clausification</i>
<blockquote>
<i class="g">Clausification</i> is the process of translating a formula
into a conjunction of clauses. A standard way is
NNF conversion, Skolemization, moving universal quantifiers
to the top (renaming bound variables if necessary),
CNF conversion, and finally removing universal quantifiers.
The variables in each resulting clause are implicitly
universally quantified.
<p>
Each step produces an equivalent formula, except for
Skolemization, which produces an equiconsistent formula,
so the result of Clausification is inconsistent iff
the original formula is inconsistent.
</blockquote>
<hr>
<!-- start universal closure -->
<a name="universal_closure">
<i>Universal Closure</i>
<blockquote>
The <i class="g">universal closure</i> of a formula is constructed by universally
quantifying, at the top of the formula, all free variables
in the formula.
</blockquote>
<hr>
<hr>
<h2>Term Ordering Terminology</h2>
<hr>
<!-- start def kbo -->
<!-- start def KBO -->
<a name="KBO">
<i>Knuth-Bendix Ordering (KBO)</i>
<blockquote>
</blockquote>
<hr>
<!-- start def LPO -->
<!-- start def lpo -->
<a name="LPO">
<i>Lexicographic Path Ordering (LPO)</i>
<blockquote>
</blockquote>
<hr>
<!-- start def RPO -->
<!-- start def rpo -->
<a name="RPO">
<i>Recursive Path Ordering (RPO)</i>
<blockquote>
</blockquote>
<hr>
<!-- start def maximal -->
<!-- start def maximal literal -->
<!-- start def maximal literals -->
<a name="maximal">
<i>Maximal Literal</i>
<blockquote>
A literal is <i class="g">maximal</i> in a clause, with respect to some term ordering,
if no literal in the clause is greater. The terms orderings used
by Prover9 (LPO, KBO, RPO) are, in general, only partial, so clauses
do not necessarily have greatest literals.
</blockquote>
<hr>
<hr>
<h2>Inference and Simplification Rules</h2>
<hr>
<!-- start def completeness -->
<a name="completeness">
<i>Completeness</i>
<blockquote>
An inference system is <i class="g">complete</i> if it is capable
(given enough time and memory) of proving any theorem
(in the language of the inference system).
</blockquote>
<hr>
<!-- start def binary resolution -->
<!-- start def resolution -->
<!-- start def positive resolution -->
<!-- start def negative resolution -->
<!-- start def positive binary resolution -->
<!-- start def negative binary resolution -->
<a name="Binary Resolution">
<i>Binary Resolution</i>
<blockquote>
The inference rule <i class="g">binary resolution</i>
takes two clauses containing
unifiable literals of opposite sign and produces a clause
consisting of the remaining literals to which the most general
unifying substitution has been applied. The rule can be viewed
as a generalization of modus ponens.
<p>
Restrictions on Binary Resolution.
<ul>
<li><i class="g">Positive resolution</i>: one of the parents is is a positive clause.
<li><i class="g">Negative resolution</i>: one of the parents is is a negative clause.
<li><i class="g">Unit resolution</i>: one of the parents is is a unit clause.
</ul>
</blockquote>
<hr>
<!-- start def ordered resolution -->
<!-- start def ordered paramodulation -->
<!-- start def literal selection -->
<a name="ordered-inf">
<i>Ordered Inference, Literal Selection</i>
<blockquote>
<i class="g">Ordered Inference</i> is a restriction of resolution
or paramdulation based on literal ordering. In some cases,
inferences can be restricted to <a href="glossary.html#maximal">maximal literals</a>.
<p>
<i class="g">Literal selection</i> is a restriction of resolution
or paramdulation. In each clause, some subset of the
negative literals are marked as selected (the selection
may be arbitrary), and in some cases inferences can be
restricted to selected literals.
</blockquote>
<hr>
<!-- start def factoring -->
<!-- start def binary factoring -->
<!-- start def factor -->
<!-- start def factorization -->
<a name="factoring">
<i>Factoring</i>
<blockquote>
The inference rule <i class="g">factoring</i> takes one clause containing two or more
literals (of the same sign) that all unify. The most general unifying
substitution is applied to the parent, and the unified literals
become identical and are merged into one.
<p>
Factoring in Prover9 is binary, operating on two literals
at a time.
</blockquote>
<hr>
<!-- start def hyperresolution -->
<!-- start def negative hyperresolution -->
<!-- start def nucleus -->
<!-- start def satellite -->
<a name="hyperresolution">
<i>Hyperresolution</i>
<blockquote>
The <i class="g">hyperresolution</i> inference rule
(also called positive hyperresolution)
takes a non-positive clause (called the
<i class="g">nucleus</i>) and simultaneously resolves each of its negative
literals with positive clauses (called the <i class="g">satellites</i>),
producing a positive clause. Hyperresolution can be viewed as a
sequence of positive binary resolution steps ending with a positive
clause.
<p>
Negative hyperresolution is similar to hyperresolution but with the
signs reversed.
</blockquote>
<hr>
<!-- start def UR-resolution -->
<!-- start def positive UR-resolution -->
<!-- start def negative UR-resolution -->
<!-- start def unit-resulting resolution -->
<a name="UR-resolution">
<i>UR-Resolution</i>
<blockquote>
The <i class="g">UR-resolution</i>
(unit-resulting resolution) inference rule takes a nonunit
clause (called the <i class="g">nucleus</i>) and resolves all but one of its literals
with unit clauses (called the <i class="g">satellites</i>), producing a unit clause.
<p>
<i class="g">Positive UR-resolution</i> is UR-resolution with the constraint that the
result must be a positive unit clause.
<p>
<i class="g">Negative UR-resolution</i> is UR-resolution with the constraint that the
result must be a negative unit clause.
</blockquote>
<hr>
<!-- start def paramodulation -->
<!-- start def from parent -->
<!-- start def from clause -->
<!-- start def from literal -->
<!-- start def into term -->
<!-- start def into parent -->
<!-- start def into clause -->
<!-- start def into literal -->
<!-- start def into term -->
<!-- start def superposition -->
<a name="from-into">
<i>"From" and "Into" in Paramodulation</i>
<blockquote>
A <i class="g">paramodulation</i> inference consists of
two parents and a child.
The parent containing the equality used for the
replacement is the <i class="g">from</i> parent or the <i class="g">from clause</i>,
the equality is the <i class="g">from</i> literal,
and the side of the equality that unifies with
the term being replaced is the <i class="g">from</i> term.
<p>
The replaced term is the <i class="g">into</i> term,
the literal containing the replaced term
is the <i class="g">into</i> literal, and
the parent containing the replaced term is the
<i class="g">into</i> parent or <i class="g">into</i> clause.
<p>
<i class="g">Superposition</i> is a restricted form of paramodulation
in which substitution is not allowed into the
lighter side of an equation.
</blockquote>
<hr>
<!-- start def positive paramodulation -->
<a name="positive-paramodulation">
<i>Positive Paramodulation</i>
<blockquote>
<i class="g">Positive paramodulation</i> is a restriction
of paramodulation in which the "from" clause is positive,
and if the "into" literal is positive, the "into" clause
is also positive.
</blockquote>
<hr>
<!-- start def demodulation -->
<!-- start def demodulator -->
<!-- start def rewriting -->
<!-- start def back demodulation -->
<!-- start def demodulator -->
<a name="demodulation">
<i>Demodulation, Back Demodulation</i>
<blockquote>
<i class="g">Demodulation</i> (also called <i class="g">rewriting</i>) is the process
of using a set of oriented equations
(demodulators) to rewrite (simplify, canonicalize) terms.
If the demodulators have good properties, demodulation terminates.
<p>
</i>Forward demodulation</i> (or just demodulation) is the process of using
a set of demodulators to rewrite newly generated clauses.
<p>
<i class="g">Back demodulation</i> is the process of using a new demodulator to
simplify previously stored clauses.
</blockquote>
<hr>
<!-- start def unit deletion -->
<!-- start def back unit deletion -->
<a name="unit-deletion">
<i>Unit Deletion, Back Unit Deletion</i>
<blockquote>
<i class="g">Unit deletion</i> is analogous to demodulation. The difference is
that unit clauses, rather than equations, are used for simplification.
<p>
Unit deletion is the process of using unit clauses to remove literals
from newly generated clauses.
<p>
<i class="g">Back unit deletion</i> is the process of using a new unit clause to
remove literals from previously stored clauses.
</blockquote>
<hr>
<!-- start def subsume -->
<!-- start def subsumption -->
<!-- start def back subsumption -->
<!-- start def forward subsumption -->
<a name="subsumption">
<i>Subsumption, Forward and Backward Subsumption</i>
<blockquote>
Clause C <i class="g">subsumes</i> clause D if the variables of C can be
instantiated in such a way that it becomes a subclause of D.
If C subsumes D, then D can be discarded, because it is weaker
than or equivalent to C. (There are some proof procedures that
require retention of subsumed clauses.)
<p>
<i class="g">Forward subsumption</i> (or just subsumption) is the process of
deleting a newly derived clause if it is subsumed by some
previously stored clause.
<p>
<i class="g">Back subsumption</i> is the process of deleting all previously stored
clauses that are subsumed by a newly derived clause.
</blockquote>
<hr>
<!-- start def unit conflict -->
<a name="conflict">
<i>Unit Conflict</i>
<blockquote>
<i class="g">Unit Conflict</i> is an inference rule that derives
a contradiction from unit clauses, for example, from
<tt>P(a,b)</tt> and <tt>-P(x,b)</tt>.
</blockquote>
<hr>
<hr>
<h2>Prover9 Terminology</h2>
<hr>
<!-- start def given clause -->
<!-- start def given clause algorithm -->
<!-- start def given clause loop -->
<!-- start def given clauses -->
<a name="given-clause">
<i>Given Clause</i>
<blockquote>
The <i class="g">given clause loop</i> drives the inference process
int Prover9. At each iteration of the loop, a <i class="g">given clause</i>
is selected from the
<a href="glossary.html#sos-usable">sos list</a>, moved the the
<a href="glossary.html#sos-usable">usable list</a>, and
then inferences are made using the given clause and other
clauses in the usable list.
</blockquote>
<hr>
<!-- start def assumptions -->
<!-- start def assumptions list -->
<!-- start def sos -->
<!-- start def sos list -->
<!-- start def usable -->
<!-- start def usable list -->
<a name="sos-usable">
<i>Sos List, Assumptions List, Usable List</i>
<blockquote>
During the search, the <i class="g">usable</i> list is the list of clauses that
are available for making inferences with the
<a href="glossary.html#given-clause">given clause</a>, and
the <i class="g">sos list</i> is the list of clauses that
are waiting to be selected as
<a href="glossary.html#given-clause">given clause</a>s.
Clauses in the sos list are not available for making primary inferences,
but they can be used to simplify inferred clauses by
<a href="glossary.html#demodulation">demodulation</a> and
<a href="glossary.html#unit-deletion">unit deletion</a>.
<p>
The <i class="g">assumptions list</i> is identical to the sos list; that is,
"assumptions" is a synonym for "sos".
<p>
Prover9 also accepts non-clausal formulas in lists named usable or sos.
Such formulas are transformed to clauses which are placed in the
clause list of the same name.
<p>
The name "sos" is used because it can be employed to achieve the
set-of-support strategy, which requires that all lines of reasoning
start with a subset of the input clauses called the set of support.
The clauses or formulas in the initial set of support are placed
the sos list, and the rest of the clauses or formulas are placed in the
usable list.
</blockquote>
<hr>
<!-- start def goal -->
<!-- start def goals list -->
<!-- start def goals -->
<a name="goals">
<i>Goal, Goals List</i>
<blockquote>
A <i class="g">goal</i> is the conclusion of a conjecture, stated in positive form.
Each goals is transformed to clauses by constructing its
<a href="glossary.html#">universal closure</a>,
negation, then
<a href="glossary.html#clausification">clausification</a>.
<p>
If there is more than one goal, Prover9 may impose restrictions
on the structure of the goals.
</blockquote>
<hr>
<!-- start def hint -->
<!-- start def hints list -->
<!-- start def hints -->
<a name="hints">
<i>Hint, Hints List</i>
<blockquote>
<i class="g">Hints</i> are clauses that are intended to guide Prover9 toward proofs.
Hints are not part of the problem specification; that is, they
are not used for making inferences. They are used only as
a component of the weighting function for selecting <a href="glossary.html#given-clause">given clauses</a>.
</blockquote>
<hr>
<!-- start def initial clause -->
<!-- start def input clause -->
<a name="initial">
<i>Initial Clause</i>
<blockquote>
A clause is an <i class="g">initial clause</i> if it exists at the
time when the first <a href="glossary.html#given-clause">given clause</a> is selected.
Initial clauses are not necessarily input clauses, because
they may be created during preprocessing, for example, by
<a href="glossary.html#demodulation">rewriting</a> or <a href="glossary.html#clausification">clausification</a>.
</blockquote>
<hr>
<!-- start def denial -->
<!-- start def denials list -->
<!-- start def denials -->
<a name="denials">
<i>Denial</i>
<blockquote>
In Prover9 terminology, a
<a href="glossary.html#clause-signs">negative clause</a>
in a </g>Horn set</g> is
called a <i class="g">denial</i>, because such clauses usually come from the
negation of a conclusion.
(The term does not apply to non-Horn sets, because a proof of a non-Horn
set may require more than one negative clause.)
</blockquote>
<hr>
<!-- start def fof reduction -->
<a name="fof-reduction">
<i>FOF Reduction</i>
<blockquote>
<i class="g">FOF (First-Order Formula) reduction</i> is a method of attempting to
simplify a problem by reducing it to an equivalent set of
independent subproblems. A trivial example is to reduce the
conjecture <tt>A <-> B</tt> to the pair of problems
<tt>A -> B</tt> and <tt>B -> A</tt>.
</blockquote>
<hr>
<!-- start def lex-dependent demodulator -->
<!-- start def lex-dependent demodulation -->
<a name="lex-dep">
<i>Lex-Dependent Demodulator</i>
<blockquote>
A <i class="g">lex-dependent demodulator</i> is one that cannot be oriented by
the primary term ordering (LPO or KBO). An example is commutativity
of a binary operation. During demodulation, a lex-dependent demodulator
is applied only if it produces a term that is smaller in the primary
term ordering.
</blockquote>
<hr>
<!-- start def depth of the term -->
<!-- start def depth of the atom -->
<!-- start def depth of the literal -->
<!-- start def depth of the clause -->
<!-- start def depth(C) -->
<a name="depth-C">
<i>Depth of Term, Atom, Literal, Clause</i>
<blockquote>
<ul>
<li>depth of variable, constant, or propositional atom: 0;
<li>depth of term or atom with arguments: one more than the maximum argument depth;
<li>depth of literal: depth of its atom (negation signs don't count);
<li>depth of clause: maximum of depths of literals;
</ul>
For example, <tt>p(x) | -p(f(x))</tt> has depth 2.
</blockquote>
<hr>
<!-- start def relational definition -->
<a name="relational-def">
<i>Relational Definition</i>
<blockquote>
A <i class="g">relational definition</i>
for an <i>n</i>-ary relation
(say <tt>P</tt> with <i>n</i>=3) is a
<a href="glossary.html#quantifiers">closed formula</a> of the form
(using Prover9 syntax)
<blockquote>
<tt>all x all y all z (P(x,y,z) <-> <i class="g">f</i>)</tt>
</blockquote>
for some formula <i>f</i> that does not contain the symbol <tt>P</tt>.
</blockquote>
<hr>
<!-- start def equational definition -->
<a name="equational-def">
<i>Equational Definition</i>
<blockquote>
An <i class="g">equational definition</i> for an <i>n</i>-ary function
(say <tt>f</tt> with <i>n</i>=3) is an equation
(using Prover9 syntax)
<blockquote>
<tt>f(x,y,z) = <i class="g">t</i></tt>
</blockquote>
for some term <i>t</i> that does not contain the symbol <tt>f</tt>
and that does not contain free variables other than
<tt>x</tt>, <tt>y</tt>, and <tt>z</tt>.
</blockquote>
<hr>
Next Section:
<a href="references.html">References</a>
</body>
</html>
|