User: Anonymous
Login
Main Menu
> Primitive Rule Specifications
Primitive Rule
Rule Specification
Specification Language
Assumption
|- p;; (Sent p)
Proof Protocol for Deductive Reasoning (PPDR)
Binary Resolution
'(or ' A ')', '(or' B ')' |- '(or ' A + B - A.i - B.j ')';; (Lit A B) (= A.i '(not ' B.j ')')
Proof Protocol for Deductive Reasoning (PPDR)
Bottom Level Task
Conjunction
N3
Cut
CWM-built-in function
DC-Train Agent Simulation
DC-Train Database Query
DC-Train Sensor Simulation
Demodulation
Direct assertion
|- p;; (Sent p)
Proof Protocol for Deductive Reasoning (PPDR)
DPLL affirmative-negative rule
DPLL atomic formulas elimination
DPLL unit clauses elimination
Entity Identification
Entity Mapping
Entity Recognition
EnumeratingProofStep
Extracted Entity Classification
Extraction
N3
Factoring
Frame Meta Information
Function Rule
Generalized Modus Ponens
A; '(implies (and ' A ')' q ')' |- q;; (Sent A q)
Proof Protocol for Deductive Reasoning (PPDR)
Generalized Modus Pones with Unification
A; '(implies ( and ' B ')' q ')' |- q[s];; (Sent A B q) (= s mgsu(A,B)) (= card(A) card(B))
Proof Protocol for Deductive Reasoning (PPDR)
Generic Web Service
Gerona Forward Chaining
Gerona
Have Effect Service
(=> (and (needEffect ?s ?c) (needNonfuncRestrs ?s ?d) (hasEffect ?r ?c) (hasNonfuncRestrs ?r ?d)) (haveEffectService ?s ?r))
Knowledge Interchange Format (KIF)
Hyperresolution
Inference
N3
InferredValueReasoningStep
Meet Service Postcondition
(=> (and (needOutput ?s ?b) (hasOutput ?r ?z) (haveTranslation ?z ?b)) (meetServicePostcondition ?s ?r))
Knowledge Interchange Format (KIF)
Meet Service Precondition
(=> (and (haveInput ?s ?a)) (hasInput ?r ?x) (haveTranslation ?a ?x)) (meetServicePrecondition ?s ?r))
Knowledge Interchange Format (KIF)
Membership Rule
Membership via Value Link
MembershipThruLinkSte
ND and elimination
'(and ' p q ')' |- p;; (Sent p q)
Proof Protocol for Deductive Reasoning (PPDR)
ND and introduction
ND implication introduction
p, [q] |- '(implies ' q p ')';; (sent p q)
Proof Protocol for Deductive Reasoning (PPDR)
ND modus ponens
p; '(implies ' p q ')' |- q;; (Sent p q)
Proof Protocol for Deductive Reasoning (PPDR)
ND Modus Pones with Unification
p; '(implies ' r q ')' |- q[s];; (Sent p q) (= s mgu(p,r))
Proof Protocol for Deductive Reasoning (PPDR)
ND or elimination
'(or ' p q ')'; r, [p]; r,[q] |- r;; (Sent p q r)
Proof Protocol for Deductive Reasoning (PPDR)
ND universal instantiation
'(forall (' N ')' q ')' |- '(forall (' N - N.i ')' q[t/N.i] ')';; (Name N) (Sent q) (Term t)
Proof Protocol for Deductive Reasoning (PPDR)
Negated Conclusion
Negative Paramodulation
Paramodulation
Reformulation
Relation Algebra Multi-Relation Union
Relation Annotation Argument Identification
Relation Identification
Relation Mapping
Relation Recognition
Relational Algebra Join
Relational Algebra Projection
Relational Algebra Selection
RuleCreationProofStep
RuleInstallationProofStep
Service Chain Success
(=> (and (haveEffectService ?s ?r) (meetPreconditionForService ?s ?r) (meetPostConditionForService ?s ?r)) (serviceChainSuccess ?s ?r))
Knowledge Interchange Format (KIF)
Source Data Access
Subsumption Rule
Target Entity Classification
Task Completed Predecessors
Task Executing
Task Finished
Task Implementing Procedure Instance
Task Instance Precondition
Task Meet Intention Preconditions
Task Meet Procedure Preconditions
Task Not Meet Termination Conditions
Task Not Successful
Task Parent Support
Task Procedure Precondition Met
Task Self Support
Task Termination Condition Met
Task Top Level Goal
Task Top-Level Goal Support
Task Unfinished
Time Point for Temporal Reasoning
Time Point Mapping
TranslationReasoningStep
Unit Deletion
Unregistered Rule
UR-Resolution
Value Collection Listener Creation
Value Link Creation
Inference Web: [
Home
|
Spec
|
Browser
|
IWBase
|
Registrar
|
Registry
]
Copyright 2008 Inference Web group.
All Rights Reserved.