type ClosedWorldProver
source code
object --+
|
api.TheoremToolCommand --+
|
api.TheoremToolCommandDecorator --+
|
object --+ |
| |
api.TheoremToolCommand --+ |
| |
api.ProverCommand --+
|
api.ProverCommandDecorator --+
|
ClosedWorldProver
This is a prover decorator that completes predicates before
proving.
If the assumptions contain "P(A)", then "all x.(P(x)
-> (x=A))" is the completion of "P". If the assumptions
contain "all x.(ostrich(x) -> bird(x))", then "all
x.(bird(x) -> ostrich(x))" is the completion of "bird".
If the assumptions don't contain anything that are "P", then
"all x.-P(x)" is the completion of "P".
walk(Socrates) Socrates != Bill + all x.(walk(x) -> (x=Socrates))
---------------- -walk(Bill)
see(Socrates, John) see(John, Mary) Socrates != John John != Mary +
all x.all y.(see(x,y) -> ((x=Socrates & y=John) | (x=John &
y=Mary))) ---------------- -see(Socrates, Mary)
all x.(ostrich(x) -> bird(x)) bird(Tweety) -ostrich(Sam) Sam !=
Tweety + all x.(bird(x) -> (ostrich(x) | x=Tweety)) + all
x.-ostrich(x) ------------------- -bird(Sam)
|
|
|
|
|
_make_unique_signature(self,
predHolder)
This method figures out how many arguments the predicate takes and
returns a tuple containing that number of unique variables. |
source code
|
|
|
|
_make_antecedent(self,
predicate,
signature)
Return an application expression with 'predicate' as the predicate
and 'signature' as the list of arguments. |
source code
|
|
|
|
|
|
|
| _map_predicates(self,
expression,
predDict) |
source code
|
|
|
Inherited from api.ProverCommandDecorator:
__init__,
decorate_proof,
get_prover,
proof,
prove
Inherited from api.TheoremToolCommandDecorator:
add_assumptions,
goal,
print_assumptions,
retract_assumptions
|
|
Create a dictionary of predicates from the assumptions.
- Parameters:
assumptions - a list of Expressions - Returns:
dict mapping AbstractVariableExpression
to PredHolder
|