Prophet/prophet.man at master · RepositoryBackups/Prophet · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
NAME
	prophet - experimental tool for computing relevance of formulas in FOF

SYNOPSIS
	prophet -p FILE [options]

OPTIONS
	-p FILE		compute relevance for formulas in FILE

   Direct relevance related
	-d 		direct relevance measure
	   union	intersection of symbols / union of symbols
           [source]	intersection of symbols / symbols in source formula
	-w 		weight of a symbol (or a variable)
           trivial   	1
           [formula]   	1 - (# of formulae with the symbol / # of formulae)
           global    	1 - (total occurrence of the symbol / # of symbols)
	   flog		- log10(# of formulae with the symbol / # of formulae)
	-v 		handling of the variables (for direct relevance)
			note: existential variables are converted to universal
	   [ignore]	disregard variables altogether
	   unique	universal variables are unique
	   similar	universal variables are similar to one another

   Indirect relevance related
	-s		handling of functors and predicates relationship
	   [join]	use together
	   split	use separately, combine final scores
	   merge	use separately, merge direct relevance (on maximum)
	-i XYZ		indirect relevance measure methods
	   X: 		estimating path length (p)
	   Y: 		calculating relevance based on a path (d)
	   Z: 		combining predicate and functor relevance value (t)

   Clustering related
	-n INTEGER	number of desired clusters (final might be smaller)
	-c		clustering method
	   indirect	use isodata algorithm on final (indirect) relevances
	   [direct]	finds fuzzy maximal cliques from direct relevance values

   Debugging
	-g STRING	list of solution formulae names separated by space
	-TEXT		output debugging information (text)
	-GRAPH		generate graph of relevance (DOT format)
        -FULLG          generate links between nodes in the same cluster
	clustered: dot -Tgif agraph.dot -o agraph.gif
	symmetric: neato -Gpack -Tgif agraph.dot -o agraph.gif

TEMPLATES
	The following combinations of possible options are merely examples
	of how prophet can be used. They are ordered by efficiency (as
	shown in empirical experiments). The topmost variant is the default.
	add < -p FILE > to every example to make it work.

Name		Call
default		-d source -w formula -v ignore -s join -i kdt -n 7 -c direct
simple		-d union -w trivial -v ignore -s split -i ppt -n 7 -c indirect

AUTHOR
	Yury Puzis (C) 2004 and the ART team