Orbital library

## orbital.moon.logic.resolution Class ResolutionBase

```java.lang.Object
orbital.moon.logic.resolution.ResolutionBase
```
All Implemented Interfaces:
Inference
Direct Known Subclasses:
SaturationResolution, SearchResolution, SetOfSupportResolution

`public abstract class ResolutionBaseextends java.lang.Objectimplements Inference`

Basic skeleton for resolution theorem provers.

General resolution procedure for M1,...,Mn ⊨ A is

1. E := {ClM1,...,ClM1,¬ClA}
2. transform each formula in E to prenex normal form
3. transform each formula in E to Skolem normal form with matrices in conjunctive normal form. The Skolem-functions introduced are new and distinct.
4. drop the ∀-quantifiers and write the remaining conjunctions of disjunctions of literals as sets of clauses. The union of these clauses is (again) called E.
5. try to resolve from E (with building variants to achieve disjunct variables) the empty clause □. Use a refinement or stronger variant of the following nondeterministic procedure:
```     R := E
while □∉R do
if there are clauses C1,C2∈R, and a variable renaming ρ
with Resolvent(C1, ρ(C2)) ∉ R
then
choose such clauses C1,C2∈R, and
choose such a variable renaming ρ
R := R∪{Resolvent(C1, ρ(C2))}
else
return fail
fi
end
return success
```

Author:
André Platzer

Constructor Summary
`ResolutionBase()`

Method Summary
`protected static ClausalFactory` `getClausalFactory()`

` boolean` ```infer(Formula[] B, Formula D)```
Apply the inference relation |~ according to the implementation calculus K.
` boolean` `isComplete()`
Whether the calculus K underlying this object to implement the inference relation is complete.
` boolean` `isSound()`
Whether the calculus K underlying this object to implement the inference relation is sound.
`protected abstract  boolean` ```prove(ClausalSet knowledgebase, ClausalSet query)```
Try to prove or disprove the conjecture.
` void` `setVerbose(boolean newVerbose)`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Constructor Detail

### ResolutionBase

`public ResolutionBase()`
Method Detail

### getClausalFactory

`protected static ClausalFactory getClausalFactory()`

### setVerbose

`public void setVerbose(boolean newVerbose)`
Add verbosity, i.e. print out a proof tree.

### infer

```public boolean infer(Formula[] B,
Formula D)```
Apply the inference relation |~ according to the implementation calculus K.

Specified by:
`infer` in interface `Inference`
Parameters:
`B` - the premises, i.e. basic knowledge formulas assumed true for the inference. Use an array of length `0` or `null` to denote the inference "∅ |~ w" from the empty set of knowledge ∅. Only axioms are available then, and thus the result is equal to that of "`true` |~ d". This inference from the empty set is abbreviated as "|~ w" because it will only infer tautologies.
`D` - the conclusion claimed, i.e. the formula to deduce from w, if possible.
Returns:
whether w |~ d, that is whether d can be inferred from the facts in w, or not.
Template Method

### isSound

`public boolean isSound()`
Description copied from interface: `Inference`
Whether the calculus K underlying this object to implement the inference relation is sound.
The calculus K is
sound
if |~|≈, i.e. if W |~ F implies W |≈ F.

Specified by:
`isSound` in interface `Inference`

### isComplete

`public boolean isComplete()`
Description copied from interface: `Inference`
Whether the calculus K underlying this object to implement the inference relation is complete.
The calculus K is
complete
if |≈|~, i.e. if W |≈ F implies W |~ F.

Specified by:
`isComplete` in interface `Inference`

### prove

```protected abstract boolean prove(ClausalSet knowledgebase,
ClausalSet query)```
Try to prove or disprove the conjecture.

Parameters:
`knowledgebase` - knowledge base W assumed consistent. W is kept in clausal normal form, and thus contains sets of literals.
`query` - the query &lnot;D, i.e. negated goal D forming the initial set of support.
Returns:
whether W ¬ &lnot;D is inconsistent, i.e. W |~ D holds.

Orbital library
1.3.0: 11 Apr 2009