IWBase core logo
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 2009 Inference Web group.
All Rights Reserved.
IW Webmaster