User: Anonymous Login

Main Menu > Use of Rules by Inference Engines

Inference Rule	Inference Engine
Assumption	Ayane 1.1 EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre Humans JTP - KSL Java Theorem Prover Metis 2.1 Metis 2.2 Semantic Discovery Service SInE 0.3 SInE 0.4 SNARK - SRI New Automated Reasoning Kit SNARK 20070805r043 SNARK 20080805r005 SNARK 20080805r018b Vampire 10.0 Vampire 11.0 Vampire 9.0 VampireLT 10.0 Waldmeister C09a
Atom1	CSD-UOC hy566
Atom2	CSD-UOC hy566
Ayane convert	Ayane 1.1
Ayane factor	Ayane 1.1
Ayane para	Ayane 1.1
Ayane resolve	Ayane 1.1
Binary Resolution	Otter SNARK - SRI New Automated Reasoning Kit
Body	CSD-UOC hy566
CWM-built-in function	CWM - W3C Semantic Web Closed World Machine
DC-Train Agent Simulation	DC-Train 4.0
DC-Train Database Query	Gerona Agent Framework
DC-Train Sensor Simulation	DC-Train 4.0
Defeasible Rule	CSD-UOC hy566
Demodulation	JTP - KSL Java Theorem Prover
Direct assertion	Ayane 1.1 CWM - W3C Semantic Web Closed World Machine DC-Train 4.0 EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre Faust 1.0 GEON Gravity Data Repository Access Service Gerona Agent Framework Humans JTP - KSL Java Theorem Prover KM - The Knowledge Machine LAPDOG Metis 2.1 Metis 2.2 Otter 3.3 SCOTT 6.1 Semantic Discovery Service SInE 0.3 SInE 0.4 SNARK - SRI New Automated Reasoning Kit SNARK 20070805r043 SNARK 20080805r005 SNARK 20080805r018b SOS 2.0 SPASS 3.01 SPASS 3.5 SPASS 3.5c Tailor Task Learner Vampire 10.0 Vampire 11.0 Vampire 9.0 VampireLT 10.0 Waldmeister C09a
DPLL affirmative-negative rule	JSAT - The Java SATisfiability Library
DPLL atomic formulas elimination	JSAT - The Java SATisfiability Library
DPLL unit clauses elimination	JSAT - The Java SATisfiability Library
Entity Identification	IBM Cross-Annotator Coreference Resolver IBM GlossOnt IBM Knowledge Structures Group's Relation Detector IBM Statistical Text Analytics Group's ACE-model Annotator IBM Statistical Text Analytics Group's KDD-model Annotator IBM TAF/Talent plus a collection of miscellaneous TFST grammars
Entity Mapping	IBM Knowledge Integrator
Entity Recognition	Dummy UIM IBM Cross-Document Coreference Resolver IBM EAnnotator IBM JResporator IBM Statistical Text Analytics Group's ACE-model Annotator IBM Statistical Text Analytics Group's KDD-model Annotator IBM TAF/Talent plus a collection of miscellaneous TFST grammars IBM Talent time annotator
EP apply_def	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP ar	EP 0.999 EP 1.0 EP 1.0pre
EP assume_negation	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP cn	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP csr	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP distribute	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP ef	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP er	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP fof_nnf	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP fof_simplification	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP pm	EP 0.999 EP 1.0 EP 1.0pre EP 1.1
EP reference	EP 1.1
EP rw	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP shift_quantors	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP skolemize	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP split_conjunct	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP split_equiv	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP spm	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP sr	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EP variable_rename	EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre
EQP conflict	EQP 0.9e
EQP demod	EQP 0.9d EQP 0.9e
EQP flip	EQP 0.9d EQP 0.9e
EQP para	EQP 0.9d EQP 0.9e
Extracted Entity Classification	IBM Cross-Annotator Coreference Resolver IBM Cross-Document Coreference Resolver IBM Statistical Text Analytics Group's ACE-model Annotator IBM Statistical Text Analytics Group's KDD-model Annotator IBM TAF/Talent plus a collection of miscellaneous TFST grammars
Factoring	Otter
Faust equality_resolution	Faust 1.0
Faust forward_subsumption_resolution__equality_resolution	Faust 1.0
Faust forward_subsumption_resolution__paramodulation	Faust 1.0
Faust forward_subsumption_resolution__resolution	Faust 1.0
Faust paramodulation	Faust 1.0
Faust resolution	Faust 1.0
Faust rewrite	Faust 1.0
Faust rewrite__forward_subsumption_resolution	Faust 1.0
Frame Meta Information	JTP - KSL Java Theorem Prover
Function Rule	JTP - KSL Java Theorem Prover
Generalized Modus Ponens	CWM - W3C Semantic Web Closed World Machine JTP - KSL Java Theorem Prover
Generic Web Service	GEON Contour Map Generation Service GEON Gridder Service
Gerona Forward Chaining	Gerona Agent Framework
Have Effect Service	Semantic Discovery Service
Humans cnf	Humans
Humans conclusion	Humans
Humans consider	Humans
Humans discharge_asm	Humans
Humans hyperresolve	Humans
Humans iterative_eq	Humans
Humans let	Humans
Humans mizar_by	Humans
Humans mizar_def_expansion	Humans
Humans mizar_from	Humans
Humans percases	Humans
Humans resolve	Humans
Humans take	Humans
Hyperresolution	Otter SNARK - SRI New Automated Reasoning Kit SWI Prolog
Id_Rule	CSD-UOC hy566
Learning by Demonstration	LAPDOG
Learning By Instruction	Tailor Task Learner
Meet Service Postcondition	Semantic Discovery Service
Meet Service Precondition	Semantic Discovery Service
Membership Rule	JTP - KSL Java Theorem Prover
Membership via Value Link	JTP - KSL Java Theorem Prover
Merge Splits	Metis 2.1 Metis 2.2 SPASS 3.01 SPASS 3.5 SPASS 3.5c
Metis canonicalize	Metis 2.2
Metis clausify	Metis 2.2
Metis cnf_normalization	Metis 2.1
Metis conjunct	Metis 2.2
Metis fof_to_cnf	Metis 2.1
Metis negate	Metis 2.2
Metis resolve	Metis 2.1 Metis 2.2
Metis simplify	Metis 2.2
Metis skolemize	Metis 2.2
Metis specialize	Metis 2.2
Metis strip	Metis 2.2
Metis subst	Metis 2.1 Metis 2.2
ND and elimination	CWM - W3C Semantic Web Closed World Machine
ND and introduction	CWM - W3C Semantic Web Closed World Machine
ND modus ponens	JEOPS - The Java Embedded Object Production System
Negated Conclusion	SNARK - SRI New Automated Reasoning Kit
Negative Paramodulation	Otter
Otter back_demod	Otter 3.3
Otter binary	Otter 3.3
Otter copy	Otter 3.3
Otter demod	Otter 3.3
Otter factor	Otter 3.3
Otter factor_simp	Otter 3.3
Otter flip	Otter 3.3
Otter hyper	Otter 3.3
Otter para_from	Otter 3.3
Otter para_into	Otter 3.3
Otter propositional	Otter 3.3
Otter unit_del	Otter 3.3
Paramodulation	Otter SNARK - SRI New Automated Reasoning Kit
Reformulation	JTP - KSL Java Theorem Prover
Refutation	Ayane 1.1 EP 0.999 EP 1.0 EP 1.0pre EP 1.1 EP 1.1pre SInE 0.3 SInE 0.4 Vampire 9.0
Relation Algebra Multi-Relation Union	ISI Mediator
Relation Annotation Argument Identification	IBM EAnnotator IBM KANI holdsDuring Relation Detector IBM Knowledge Structures Group's Relation Detector IBM Statistical Text Analytics Group's ACE-model Annotator IBM Statistical Text Analytics Group's KDD-model Annotator IBM TAF/Talent plus a collection of miscellaneous TFST grammars
Relation Identification	IBM Cross-Annotator Coreference Resolver IBM Cross-Document Coreference Resolver IBM Knowledge Structures Group's Relation Detector IBM Statistical Text Analytics Group's ACE-model Annotator IBM Statistical Text Analytics Group's KDD-model Annotator IBM TAF/Talent plus a collection of miscellaneous TFST grammars
Relation Mapping	IBM Knowledge Integrator
Relation Recognition	IBM EAnnotator IBM KANI holdsDuring Relation Detector IBM Statistical Text Analytics Group's ACE-model Annotator IBM Statistical Text Analytics Group's KDD-model Annotator IBM TAF/Talent plus a collection of miscellaneous TFST grammars
Relational Algebra Join	ISI Mediator
Relational Algebra Projection	ISI Mediator
Relational Algebra Selection	ISI Mediator
SCOTT back_demod	SCOTT 6.1
SCOTT binary	SCOTT 6.1
SCOTT copy	SCOTT 6.1
SCOTT demod	SCOTT 6.1
SCOTT factor	SCOTT 6.1
SCOTT factor_simp	SCOTT 6.1
SCOTT flip	SCOTT 6.1
SCOTT hyper	SCOTT 6.1
SCOTT para_from	SCOTT 6.1
SCOTT para_into	SCOTT 6.1
SCOTT propositional	SCOTT 6.1
SCOTT unit_del	SCOTT 6.1
SCOTT ur	SCOTT 6.1
Service Chain Success	Semantic Discovery Service
SInE apply_def	SInE 0.3 SInE 0.4
SInE assume_negation	SInE 0.3 SInE 0.4
SInE cn	SInE 0.3 SInE 0.4
SInE csr	SInE 0.3 SInE 0.4
SInE distribute	SInE 0.3 SInE 0.4
SInE ef	SInE 0.3 SInE 0.4
SInE er	SInE 0.3 SInE 0.4
SInE fof_nnf	SInE 0.3 SInE 0.4
SInE fof_simplification	SInE 0.3 SInE 0.4
SInE pm	SInE 0.3 SInE 0.4
SInE reference	SInE 0.4
SInE rw	SInE 0.3 SInE 0.4
SInE shift_quantors	SInE 0.3 SInE 0.4
SInE skolemize	SInE 0.3 SInE 0.4
SInE split_conjunct	SInE 0.3 SInE 0.4
SInE split_equiv	SInE 0.3 SInE 0.4
SInE spm	SInE 0.3 SInE 0.4
SInE sr	SInE 0.3 SInE 0.4
SInE variable_rename	SInE 0.3 SInE 0.4
SNARK CONDENSE	SNARK 20070805r043 SNARK 20080805r005 SNARK 20080805r018b
SNARK EMBED	SNARK 20070805r043 SNARK 20080805r005 SNARK 20080805r018b
SNARK FACTOR	SNARK 20070805r043 SNARK 20080805r005 SNARK 20080805r018b
SNARK HYPERRESOLVE	SNARK 20070805r043 SNARK 20080805r005 SNARK 20080805r018b
SNARK PARAMODULATE	SNARK 20070805r043 SNARK 20080805r005 SNARK 20080805r018b
SNARK REWRITE	SNARK 20070805r043 SNARK 20080805r005 SNARK 20080805r018b
SOS back_demod	SOS 2.0
SOS binary	SOS 2.0
SOS copy	SOS 2.0
SOS demod	SOS 2.0
SOS factor	SOS 2.0
SOS factor_simp	SOS 2.0
SOS flip	SOS 2.0
SOS hyper	SOS 2.0
SOS new_demod	SOS 2.0
SOS para_from	SOS 2.0
SOS para_into	SOS 2.0
SOS propositional	SOS 2.0
SOS unit_del	SOS 2.0
Source Data Access	ISI Mediator
SPASS aed	SPASS 3.01 SPASS 3.5 SPASS 3.5c
SPASS con	SPASS 3.01 SPASS 3.5
SPASS ems	SPASS 3.01 SPASS 3.5
SPASS eqf	SPASS 3.01 SPASS 3.5
SPASS eqr	SPASS 3.01 SPASS 3.5
SPASS fac	SPASS 3.01 SPASS 3.5
SPASS mrr	SPASS 3.01 SPASS 3.5 SPASS 3.5c
SPASS obv	SPASS 3.01 SPASS 3.5 SPASS 3.5c
SPASS res	SPASS 3.01 SPASS 3.5
SPASS rew	SPASS 3.01 SPASS 3.5 SPASS 3.5c
SPASS sor	SPASS 3.01 SPASS 3.5
SPASS spl	SPASS 3.01 SPASS 3.5 SPASS 3.5c
SPASS spr	SPASS 3.01 SPASS 3.5 SPASS 3.5c
SPASS spt	SPASS 3.01 SPASS 3.5 SPASS 3.5c
SPASS ssi	SPASS 3.01 SPASS 3.5
SPASS unc	SPASS 3.01 SPASS 3.5 SPASS 3.5c
Strict Rule	CSD-UOC hy566
Subsumption Rule	JTP - KSL Java Theorem Prover
Super Rule	CSD-UOC hy566
Superiority Rule	CSD-UOC hy566
Task Executing	SPARK: SRI Procedural Agent Realization Kit
Task Meet Intention Preconditions	SPARK: SRI Procedural Agent Realization Kit
Task Meet Procedure Preconditions	SPARK: SRI Procedural Agent Realization Kit
Task Not Meet Termination Conditions	SPARK: SRI Procedural Agent Realization Kit
Task Not Successful	SPARK: SRI Procedural Agent Realization Kit
Task Parent Support	SPARK: SRI Procedural Agent Realization Kit
Task Self Support	SPARK: SRI Procedural Agent Realization Kit
Task Top-Level Goal Support	SPARK: SRI Procedural Agent Realization Kit
Task Unfinished	SPARK: SRI Procedural Agent Realization Kit
Time Point for Temporal Reasoning	JTP - KSL Java Theorem Prover
Time Point Mapping	JTP - KSL Java Theorem Prover
TranslationReasoningStep	JTP - KSL Java Theorem Prover
Unit Deletion	Otter
UR-Resolution	Otter
Value Collection Listener Creation	JTP - KSL Java Theorem Prover
Value Link Creation	JTP - KSL Java Theorem Prover
Vampire backward demodulation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire backward superposition	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire cnf transformation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire definition folding	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire definition unfolding	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire ENNF transformation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire equality factoring	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire equality permutation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire equality proxy replacement	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire equality resolution	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire equivalence to implication	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire flattening	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire forward demodulation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire forward subsumption resolution	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire forward superposition	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire literal permutation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire NNF transformation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire normalize	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire passive clause reanimation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire permutation	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire rectify	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire repeated literal deletion	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire resolution	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire simplification by true or false	Vampire 10.0 Vampire 11.0 Vampire 9.0
Vampire skolemization	Vampire 10.0 Vampire 11.0 Vampire 9.0
VampireLT backward demodulation	VampireLT 10.0
VampireLT backward superposition	VampireLT 10.0
VampireLT cnf transformation	VampireLT 10.0
VampireLT definition folding	VampireLT 10.0
VampireLT definition unfolding	VampireLT 10.0
VampireLT ENNF transformation	VampireLT 10.0
VampireLT equality factoring	VampireLT 10.0
VampireLT equality permutation	VampireLT 10.0
VampireLT equality proxy replacement	VampireLT 10.0
VampireLT equality resolution	VampireLT 10.0
VampireLT equivalence to implication	VampireLT 10.0
VampireLT flattening	VampireLT 10.0
VampireLT forward demodulation	VampireLT 10.0
VampireLT forward subsumption resolution	VampireLT 10.0
VampireLT forward superposition	VampireLT 10.0
VampireLT literal permutation	VampireLT 10.0
VampireLT NNF transformation	VampireLT 10.0
VampireLT normalize	VampireLT 10.0
VampireLT passive clause reanimation	VampireLT 10.0
VampireLT permutation	VampireLT 10.0
VampireLT rectify	VampireLT 10.0
VampireLT repeated literal deletion	VampireLT 10.0
VampireLT resolution	VampireLT 10.0
VampireLT simplification by true or false	VampireLT 10.0
VampireLT skolemization	VampireLT 10.0
Waldmeister activate	Waldmeister C09a
Waldmeister cp	Waldmeister C09a
Waldmeister instl	Waldmeister C09a
Waldmeister instr	Waldmeister C09a
Waldmeister interreduction_right	Waldmeister C09a
Waldmeister orient	Waldmeister C09a
Waldmeister reduction	Waldmeister C09a
Waldmeister trivial	Waldmeister C09a
Waldmeister weigh	Waldmeister C09a

Copyright 2010 Inference Web group.
All Rights Reserved.