| Inference Rule |
Rule Specification |
| Specification Language |
| Assumption |
|- p;; (Sent p) |
| Proof Protocol for Deductive Reasoning (PPDR) |
| Atom |
predicate '(' argument, ... ')' |
| |
| Atom1 |
predicate '(' (constant || variable), ... ')' |
| |
| Atom2 |
Atom1 || ~Atom1 |
| |
| Ayane convert |
|
| |
| Ayane factor |
|
| |
| Ayane para |
|
| |
| Ayane resolve |
|
| |
| 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) |
| Body |
Atom2, ... |
| |
| Bottom Level Task |
|
| |
| Business Owners Typically Have Offices |
|
| |
| Class Transitivity |
|
| |
| Conjunction |
|
| N3 |
| Cut |
|
| |
| CWM-built-in function |
|
| |
| DC-Train Agent Simulation |
|
| |
| DC-Train Database Query |
|
| |
| DC-Train Sensor Simulation |
|
| |
| Defeasible Rule |
Body => Atom2 |
| |
| Demodulation |
|
| |
| Derived Membership |
|
| |
| 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 |
|
| |
| EP apply_def |
|
| |
| EP ar |
|
| |
| EP assume_negation |
|
| |
| EP cn |
|
| |
| EP csr |
|
| |
| EP distribute |
|
| |
| EP ef |
x=a v b=c v x=d ==> a!=c v b=c v b=d |
| |
| EP er |
x!=a v x=x ==> a=a |
| |
| EP fof_nnf |
|
| |
| EP fof_simplification |
|
| |
| EP pm |
|
| |
| EP reference |
|
| |
| EP rw |
|
| |
| EP shift_quantors |
|
| |
| EP skolemize |
|
| |
| EP split_conjunct |
|
| |
| EP split_equiv |
|
| |
| EP spm |
|
| |
| EP sr |
|
| |
| EP variable_rename |
|
| |
| EQP conflict |
|
| |
| EQP demod |
|
| |
| EQP flip |
|
| |
| EQP para |
|
| |
| Extracted Entity Classification |
|
| |
| Extraction |
|
| N3 |
| Factoring |
|
| |
| Faust equality_resolution |
|
| |
| Faust forward_subsumption_resolution__equality_resolution |
|
| |
| Faust forward_subsumption_resolution__paramodulation |
|
| |
| Faust forward_subsumption_resolution__resolution |
|
| |
| Faust paramodulation |
|
| |
| Faust resolution |
|
| |
| Faust rewrite |
|
| |
| Faust rewrite__forward_subsumption_resolution |
|
| |
| 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 |
| Has Business Owns Office Typically |
|
| |
| Have Effect Service |
(=> (and (needEffect ?s ?c)
(needNonfuncRestrs ?s ?d)
(hasEffect ?r ?c)
(hasNonfuncRestrs ?r ?d))
(haveEffectService ?s ?r)) |
| Knowledge Interchange Format (KIF) |
| Humans cnf |
|
| |
| Humans conclusion |
|
| |
| Humans consider |
|
| |
| Humans discharge_asm |
|
| |
| Humans hyperresolve |
|
| |
| Humans iterative_eq |
|
| |
| Humans let |
|
| |
| Humans mizar_by |
|
| |
| Humans mizar_def_expansion |
|
| |
| Humans mizar_from |
|
| |
| Humans percases |
|
| |
| Humans resolve |
|
| |
| Humans take |
|
| |
| Hyper Translation |
|
| |
| Hyperresolution |
|
| |
| Id_Rule |
id ':' Super Rule |
| |
| Inference |
|
| N3 |
| InferredValueReasoningStep |
|
| |
| Instance of Subclass is Instance of Class |
|
| |
| Learning by Demonstration |
|
| |
| Learning By Instruction |
|
| |
| 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 |
|
| |
| Merge Splits |
|
| |
| Metis canonicalize |
|
| |
| Metis clausify |
|
| |
| Metis cnf_normalization |
|
| |
| Metis conjunct |
|
| |
| Metis fof_to_cnf |
|
| |
| Metis negate |
|
| |
| Metis resolve |
|
| |
| Metis simplify |
|
| |
| Metis skolemize |
|
| |
| Metis specialize |
|
| |
| Metis strip |
|
| |
| Metis subst |
|
| |
| 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 |
|
| |
| Not Atom |
~ predicate |
| |
| null conclusion |
|
| |
| null discharge_asm |
|
| |
| null let |
|
| |
| null mizar_by |
|
| |
| Otter back_demod |
|
| |
| Otter binary |
|
| |
| Otter copy |
|
| |
| Otter demod |
|
| |
| Otter factor |
|
| |
| Otter factor_simp |
|
| |
| Otter flip |
|
| |
| Otter hyper |
|
| |
| Otter para_from |
|
| |
| Otter para_into |
|
| |
| Otter propositional |
|
| |
| Otter unit_del |
|
| |
| Paramodulation |
|
| |
| Provisional Conclusion |
|
| |
| Query Reformulation |
|
| |
| Reformulation |
|
| |
| Refutation |
|
| |
| 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 |
|
| |
| SCOTT back_demod |
|
| |
| SCOTT binary |
|
| |
| SCOTT copy |
|
| |
| SCOTT demod |
|
| |
| SCOTT factor |
|
| |
| SCOTT factor_simp |
|
| |
| SCOTT flip |
|
| |
| SCOTT hyper |
|
| |
| SCOTT para_from |
|
| |
| SCOTT para_into |
|
| |
| SCOTT propositional |
|
| |
| SCOTT unit_del |
|
| |
| SCOTT ur |
|
| |
| Service Chain Success |
(=> (and (haveEffectService ?s ?r)
(meetPreconditionForService ?s ?r)
(meetPostConditionForService ?s ?r))
(serviceChainSuccess ?s ?r)) |
| Knowledge Interchange Format (KIF) |
| SInE apply_def |
|
| |
| SInE assume_negation |
|
| |
| SInE cn |
|
| |
| SInE csr |
|
| |
| SInE distribute |
|
| |
| SInE ef |
|
| |
| SInE er |
|
| |
| SInE fof_nnf |
|
| |
| SInE fof_simplification |
|
| |
| SInE pm |
|
| |
| SInE reference |
|
| |
| SInE rw |
|
| |
| SInE shift_quantors |
|
| |
| SInE skolemize |
|
| |
| SInE split_conjunct |
|
| |
| SInE split_equiv |
|
| |
| SInE spm |
|
| |
| SInE sr |
|
| |
| SInE variable_rename |
|
| |
| SNARK CONDENSE |
|
| |
| SNARK EMBED |
|
| |
| SNARK FACTOR |
|
| |
| SNARK HYPERRESOLVE |
|
| |
| SNARK PARAMODULATE |
|
| |
| SNARK REWRITE |
|
| |
| SOS back_demod |
|
| |
| SOS binary |
|
| |
| SOS copy |
|
| |
| SOS demod |
|
| |
| SOS factor |
|
| |
| SOS factor_simp |
|
| |
| SOS flip |
|
| |
| SOS hyper |
|
| |
| SOS new_demod |
|
| |
| SOS para_from |
|
| |
| SOS para_into |
|
| |
| SOS propositional |
|
| |
| SOS unit_del |
|
| |
| Source Data Access |
|
| |
| SPASS aed |
|
| |
| SPASS con |
|
| |
| SPASS ems |
|
| |
| SPASS eqf |
|
| |
| SPASS eqr |
|
| |
| SPASS fac |
|
| |
| SPASS mrr |
|
| |
| SPASS obv |
|
| |
| SPASS res |
|
| |
| SPASS rew |
|
| |
| SPASS sor |
|
| |
| SPASS spl |
|
| |
| SPASS spr |
|
| |
| SPASS spt |
|
| |
| SPASS ssi |
|
| |
| SPASS unc |
|
| |
| Strict Rule |
Body -> Atom2 |
| |
| Subsumption Rule |
|
| |
| Super Rule |
Atom2 || Strict Rule || Defeasible Rule |
| |
| Superiority Rule |
sup '(' superior_rule_id, inferior_rule_id ')' |
| |
| 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 |
|
| |
| Told negated_conjecture |
|
| |
| TranslationReasoningStep |
|
| |
| Unit Deletion |
|
| |
| Unregistered Rule |
|
| |
| Unzip |
|
| |
| UR-Resolution |
|
| |
| Value Collection Listener Creation |
|
| |
| Value Link Creation |
|
| |
| Vampire backward demodulation |
|
| |
| Vampire backward superposition |
|
| |
| Vampire cnf transformation |
|
| |
| Vampire definition folding |
|
| |
| Vampire definition unfolding |
|
| |
| Vampire ENNF transformation |
|
| |
| Vampire equality factoring |
|
| |
| Vampire equality permutation |
|
| |
| Vampire equality proxy replacement |
|
| |
| Vampire equality resolution |
|
| |
| Vampire equivalence to implication |
|
| |
| Vampire flattening |
|
| |
| Vampire forward demodulation |
|
| |
| Vampire forward subsumption resolution |
|
| |
| Vampire forward superposition |
|
| |
| Vampire literal permutation |
|
| |
| Vampire NNF transformation |
|
| |
| Vampire normalize |
|
| |
| Vampire passive clause reanimation |
|
| |
| Vampire permutation |
|
| |
| Vampire rectify |
|
| |
| Vampire repeated literal deletion |
|
| |
| Vampire resolution |
|
| |
| Vampire simplification by true or false |
|
| |
| Vampire skolemization |
|
| |
| VampireLT backward demodulation |
|
| |
| VampireLT backward superposition |
|
| |
| VampireLT cnf transformation |
|
| |
| VampireLT definition folding |
|
| |
| VampireLT definition unfolding |
|
| |
| VampireLT ENNF transformation |
|
| |
| VampireLT equality factoring |
|
| |
| VampireLT equality permutation |
|
| |
| VampireLT equality proxy replacement |
|
| |
| VampireLT equality resolution |
|
| |
| VampireLT equivalence to implication |
|
| |
| VampireLT flattening |
|
| |
| VampireLT forward demodulation |
|
| |
| VampireLT forward subsumption resolution |
|
| |
| VampireLT forward superposition |
|
| |
| VampireLT literal permutation |
|
| |
| VampireLT NNF transformation |
|
| |
| VampireLT normalize |
|
| |
| VampireLT passive clause reanimation |
|
| |
| VampireLT permutation |
|
| |
| VampireLT rectify |
|
| |
| VampireLT repeated literal deletion |
|
| |
| VampireLT resolution |
|
| |
| VampireLT simplification by true or false |
|
| |
| VampireLT skolemization |
|
| |
| Waldmeister activate |
|
| |
| Waldmeister cp |
|
| |
| Waldmeister instl |
|
| |
| Waldmeister instr |
|
| |
| Waldmeister interreduction_right |
|
| |
| Waldmeister orient |
|
| |
| Waldmeister reduction |
|
| |
| Waldmeister trivial |
|
| |
| Waldmeister weigh |
|
| |
Copyright 2010 Inference Web group.
All Rights Reserved.
