IFSTool - Revision history

Dimitar Dimitrov at 12:12, 9 April 2018

2018-04-09T12:12:23Z

← Older revision		Revision as of 15:12, 9 April 2018
Line 97:		Line 97:
	# The formula is checked in several values. For example, if the step is 0.5 (3 shots in the interval [0, 1]), the following values are used: <0,0>, <0,0.5>, <0,1>, <0.5,0>, <0.5,0.5>, <1,0>. If the formula is not satisfied on any of the values, it is marked as '''“not satisfied”''' and no further checks are made for it.		# The formula is checked in several values. For example, if the step is 0.5 (3 shots in the interval [0, 1]), the following values are used: <0,0>, <0,0.5>, <0,1>, <0.5,0>, <0.5,0.5>, <1,0>. If the formula is not satisfied on any of the values, it is marked as '''“not satisfied”''' and no further checks are made for it.
	# The formula is attempted to be proved by checking a large set of rules. For example, if <tt>max(x,y)>z</tt> has to be proved, it is replaced by the disjunction <tt>(x>z \| y>z)</tt>.		# The formula is attempted to be proved by checking a large set of rules. For example, if <tt>max(x,y)>z</tt> has to be proved, it is replaced by the disjunction <tt>(x>z \| y>z)</tt>.

			== Download ==

			{{download\|IFSTool.zip\|ZIP\|33}}

	[[Category:Intuitionistic fuzzy sets]]		[[Category:Intuitionistic fuzzy sets]]
	[[Category:Software]]		[[Category:Software]]

Vassia Atanassova at 15:42, 18 July 2010

2010-07-18T15:42:06Z

Vassia Atanassova: /* Checking the validity of user-defined axioms */

2010-07-18T15:37:06Z

Checking the validity of user-defined axioms

← Older revision		Revision as of 18:37, 18 July 2010
Line 50:		Line 50:
	#:: t21 (\neg A \vee B) \supset (A \supset B)		#:: t21 (\neg A \vee B) \supset (A \supset B)
	#:: ky3 (<0,1> \supset A) = <1,0></tt>		#:: ky3 (<0,1> \supset A) = <1,0></tt>
	# Set shots to be 5.		# Set shots to '''5'''.
	# Click '''"Check axioms..."'''. A new window is opened. The axioms should be visible on the left side of the window.		# Click '''"Check axioms..."'''. A new window is opened. The axioms should be visible on the left side of the window.
	# There is an option '''"Check for Intuitionistic Fuzzy Tautologies"'''. Deselect it if you want to check for non-intuitionistic tautologies (to check a expression if it is equal to <1,0>).		# There is an option '''"Check for Intuitionistic Fuzzy Tautologies"'''. Deselect it if you want to check for non-intuitionistic tautologies (to check a expression if it is equal to <1,0>).

Vassia Atanassova: /* Drawing the graph of relations */

2010-07-18T15:35:06Z

Drawing the graph of relations

← Older revision		Revision as of 18:35, 18 July 2010
Line 81:		Line 81:

	=== Drawing the graph of relations ===		=== Drawing the graph of relations ===

			[[Image:IFSTool-graph.png\|right\|thumb\|400px\|Drawing the graph of the relation "smaller or equal".]]

	To draw a graph for the relation <tt><</tt> :		To draw a graph for the relation <tt><</tt> :

Vassia Atanassova: /* Removal of duplicate operations */

2010-07-18T15:33:45Z

Removal of duplicate operations

← Older revision		Revision as of 18:33, 18 July 2010
Line 65:		Line 65:
	=== Removal of duplicate operations ===		=== Removal of duplicate operations ===

	[[Image:IFSTool-~~home~~-~~screen~~.png\|right\|thumb\|400px\|Removal of duplicates of implications or negations in IFSTool. In the example, implications No. 5,11 and 5,14 are equivalent to implication 5,3, so are given below indented.]]		[[Image:IFSTool-remove-duplicates.png\|right\|thumb\|400px\|Removal of duplicates of implications or negations in IFSTool. In the example, implications No. 5,11 and 5,14 are equivalent to implication 5,3, so are given below indented.]]

	To remove duplicate implications (or negations, respectively):		To remove duplicate implications (or negations, respectively):

Vassia Atanassova: /* Removal of duplicate operations */

2010-07-18T15:33:24Z

Removal of duplicate operations

← Older revision		Revision as of 18:33, 18 July 2010
Line 64:		Line 64:

	=== Removal of duplicate operations ===		=== Removal of duplicate operations ===

			[[Image:IFSTool-home-screen.png\|right\|thumb\|400px\|Removal of duplicates of implications or negations in IFSTool. In the example, implications No. 5,11 and 5,14 are equivalent to implication 5,3, so are given below indented.]]

	To remove duplicate implications (or negations, respectively):		To remove duplicate implications (or negations, respectively):

Vassia Atanassova: /* Checking the validity of user-defined axioms */

2010-07-18T15:31:20Z

Checking the validity of user-defined axioms

← Older revision		Revision as of 18:31, 18 July 2010
Line 24:		Line 24:

	=== Checking the validity of user-defined axioms ===		=== Checking the validity of user-defined axioms ===

			[[Image:IFSTool-check-axioms.png\|right\|thumb\|400px\|The screen for checking axioms. To the left a list of axioms is given and to the right - the results from the check. Implications are given in the rows, and axioms - in the columns. Clicking on a table cell, a window with more detailed information is being opened.]]

	To check the validity of axioms for a set of implications (or negations), you have to execute the following steps:		To check the validity of axioms for a set of implications (or negations), you have to execute the following steps:

Vassia Atanassova: /* Basic properties */

2010-07-18T15:27:29Z

Basic properties

← Older revision		Revision as of 18:27, 18 July 2010
Line 2:		Line 2:

	== Basic properties ==		== Basic properties ==

			[[Image:IFSTool-home-screen.png\|right\|thumb\|400px\|Home screen of IFSTool. A list of implications has been loaded for investigation. To the right the list of possible actions is given.]]

	Some of the properties that can be checked are the following:		Some of the properties that can be checked are the following:

Vassia Atanassova at 15:20, 18 July 2010

2010-07-18T15:20:12Z

Vassia Atanassova: New page: '''IFSTool''' is a software for checking properties of intuitionistic fuzzy implications and negations. It is being developed by Dimitar Dimitrov...

2010-07-18T15:19:12Z

New page: '''IFSTool''' is a software for checking properties of intuitionistic fuzzy implications and negations. It is being developed by Dimitar Dimitrov...

New page

'''IFSTool''' is a software for checking properties of [[intuitionistic fuzzy implications]] and [[intuitionistic fuzzy negations|negations]]. It is being developed by [[Dimitar Dimitrov]] in the frames of the bilateral scientific exchange project [[Ifigenia:Design and development of intuitionistic fuzzy logic tools in information technologies|Design and development of intuitionistic fuzzy logic tools in information technologies]]. IFSTool requires Microsoft .NET Framework (already installed on newer MS Windows versions) to run.

Some of the properties that can be checked are the following:
* Checking the validity of user-defined axioms of the classical and non-classical logics.
* Equivalence of implications and equivalence of negations.
* Order of implications and negations (generating the graph for the relation "less than or equal").

All generated data can be exported to various text and graphic formats, such as TeX, HTML, PNG and etc.

All implications (or negations, respectively) have to be imported by the user from external text files. Files should be in the following format:
* the definition of each implication/negation should be on a single line;
* no two definitions should share a single line;
* each line should begin with unique identifier of the implication/negation, followed by delimiter ("<tt>:</tt> " or tab), then the first (validity) part of the implication/negation's definition, delimiter ("<tt>,</tt> " or tab), and the second (nonvalidity) part of the implication/negation's definition;
* no spaces are allowed in the validity and nonvalidity parts;
* the left argument of the implications is <tt><a, b></tt> and the right one is <tt><c, d></tt>. For negations the argument is <tt><a,b></tt>. No other parameter names are allowed for now.

Here's a short example of a file which can be imported:
: <tt>1: max(b,min(a,c)), min(a,d)</tt>
: <tt>2: 1-sg(a-c), d*sg(a-c)</tt>

== Checking the validity of user-defined axioms ==
To check the validity of axioms for a set of implications (or negations), you have to execute the following steps:
# Click '''"Import from File"''' to load a text file with implications or negations. Several files can be imported and appended.
# Provide a text file named ''"Axioms.txt"'' in the directory where the IFSTool executable is located. The file should contain axioms in the following format:
#* each axiom definition should be on a single line;
#* no two definitions should share a single line;
#* each line should begin with unique identifier of the axiom, followed by space, and then the definition of the axiom.
#* IF variables should be named <tt>A, B, C, ..., Z</tt>. It is recommended to start with <tt>A</tt>, then <tt>B</tt>, and so on, otherwise the program will run significantly slower;
#* IF constants can be set in the form <value1,value2>.
#: The following operators can be used:
#* <tt>\supset</tt> - the current implication that is tested;
#* <tt>\neg</tt> - the corresponding negation of currently tested implication;
#* <tt>\&</tt> - intuitionistic fuzzy conjunction (<tt><a,b> \& <c,d> <=> min(a, c), max(b, d)</tt>);
#* <tt>\vee</tt> - intuitionistic fuzzy disjunction (<tt><a,b> \vee <c,d> <=> max(a, c), min(b, d)</tt>);
#* <tt>\classicnot</tt> - the classical fuzzy negation (<tt>\classicnot <a,b> <=> <nowiki><</nowiki>b,a></tt>);
#* <tt>=</tt> - equality (<tt><a,b> = <c,d> <=> a=c and b=d</tt>);
#* <tt>>=</tt> - greater-than-or-equal - (<tt><a,b> >= <c,d> <=> a>=c and b<=d</tt>)
#* <tt><=</tt> - less-than-or-equal
#: All operators should be surrounded with spaces.
#: Example file:
#:: <tt>t0 A \supset A
#:: t14 A \supset (B \supset (A \& B))
#:: t21 (\neg A \vee B) \supset (A \supset B)
#:: ky3 (<0,1> \supset A) = <1,0></tt>
# Set shots to be 5.
# Click '''"Check axioms..."'''. A new window is opened. The axioms should be visible on the left side of the window.
# There is an option '''"Check for Intuitionistic Fuzzy Tautologies"'''. Deselect it if you want to check for non-intuitionistic tautologies (to check a expression if it is equal to <1,0>).
# Click '''"Check All Axioms For All Implications"'''. This may take a lot of time, especially for relatively smaller steps (0.1 for example).
# A table with results is displayed. When clicking on a cell, the following information is displayed:
#* the tested implication;
#* the tested negation;
#* the checked axiom;
#* normalized arithmetic expression that corresponds to the axiom with the given implication and negation;
#* the status of the axiom (for the given implication and negation) - one of the following: '''“Satisfied (proved)”''', '''“Not satisfied (proved)”''' and '''“Possibly satisfied (No counterexample found)”'''.
# If there are possibly satisfied axioms, you can specify smaller step (larger number of shots) and then click '''"Check not proved with more shots"'''. Some of the possibly satisfied axioms may turn to '''"Not satisfied (proved)"'''. The rest should be proved manually (in next versions of the software this is going to be improved).
# By default, each axiom is tested with all implications and their corresponding negations. If '''"Use only corresponding negations"''' is unchecked, all axioms will be checked for all combinations of implications and negations.

== Removal of duplicate operations ==

To remove duplicate implications (or negations, respectively):
# '''Import''' the implications/negations.
# Set shots = '''5'''.
# Click '''"Remove duplicates"'''. A detailed report is generated showing the groups of equivalent and possibly equivalent implications/negations.
# Check the lines marked with '''"(not proved)"'''. If there are different implications/negations, marked as equivalent, go back to step 2 and specify bigger number.
# Click '''"Remove duplicates"'''. There is an option for renumbering the implications/negations, since the initial numbering may not be continuous after removing some implications/negations.

To check if a new intuitionistic fuzzy implication (or negation, respectively) is not equivalent to some old one, the following approach can be used:
# Import all intuitionistic fuzzy implications/negations.
# Remove the duplicates, as described above.
# Import the new implication/negation and remove the duplicates again.
# If the new implication/negation is equivalent to some old one, this could be seen in the report window.

== Drawing the graph of relations ==

To draw a graph for the relation <tt><</tt> :
# Import the implications or negations.
# Set shots to be '''5''' or more.
# Click '''“Draw graph for the relation “less than or equal””'''. This may take some time.
# By default, a transitive reduction is applied, since the relation < is transitive. If i1 < i2 and i2 < i3, the corresponding ribs are colored in black and the rib from i1 to i3 is colored in gray.

== Algorithm ==

IFSTool uses binary trees to represent the expressions.
When a formula has to be checked:
# The formula is optimized as much as possible. For example, a*(b-b) is equivalent to 0. Many IF-specific optimizations are performed.
# The formula is checked in several values. For example, if the step is 0.5 (3 shots in the interval [0, 1]), the following values are used: <0,0>, <0,0.5>, <0,1>, <0.5,0>, <0.5,0.5>, <1,0>. If the formula is not satisfied on any of the values, it is marked as “not satisfied” and no further checks are made for it.
# The formula is attempted to be proved by checking a large set of rules. For example, if max(x,y)>z has to be proved, it is replaced by the disjunction (x>z | y>z).

[[Category:Intuitionistic fuzzy sets]]
[[Category:Software]]

← Older revision		Revision as of 18:42, 18 July 2010
Line 34:		Line 34:
	#* each line should begin with unique identifier of the axiom, followed by space, and then the definition of the axiom.		#* each line should begin with unique identifier of the axiom, followed by space, and then the definition of the axiom.
	#* IF variables should be named <tt>A, B, C, ..., Z</tt>. It is recommended to start with <tt>A</tt>, then <tt>B</tt>, and so on, otherwise the program will run significantly slower;		#* IF variables should be named <tt>A, B, C, ..., Z</tt>. It is recommended to start with <tt>A</tt>, then <tt>B</tt>, and so on, otherwise the program will run significantly slower;
	#* IF constants can be set in the form <value1,value2>.		#* IF constants can be set in the form <tt><value1,value2></tt>.
	#: The following operators can be used:		#: The following operators can be used:
	#* <tt>\supset</tt> - the current implication that is tested;		#:* <tt>\supset</tt> : the current implication that is tested;
	#* <tt>\neg</tt> - the corresponding negation of currently tested implication;		#:* <tt>\neg</tt> : the corresponding negation of currently tested implication;
	#* <tt>\&</tt> - intuitionistic fuzzy conjunction (<tt><a,b> \& <c,d> <=> min(a, c), max(b, d)</tt>);		#:* <tt>\&</tt> : intuitionistic fuzzy conjunction (<tt><a,b> \& <c,d> <=> min(a, c), max(b, d)</tt>);
	#* <tt>\vee</tt> - intuitionistic fuzzy disjunction (<tt><a,b> \vee <c,d> <=> max(a, c), min(b, d)</tt>);		#:* <tt>\vee</tt> : intuitionistic fuzzy disjunction (<tt><a,b> \vee <c,d> <=> max(a, c), min(b, d)</tt>);
	#* <tt>\classicnot</tt> - the classical fuzzy negation (<tt>\classicnot <a,b> <=> <nowiki><</nowiki>b,a></tt>);		#:* <tt>\classicnot</tt> : the classical fuzzy negation (<tt>\classicnot <a,b> <=> <nowiki><</nowiki>b,a></tt>);
	#* <tt>=</tt> - equality (<tt><a,b> = <c,d> <=> a=c and b=d</tt>);		#:* <tt>=</tt> : equality (<tt><a,b> = <c,d> <=> a=c and b=d</tt>);
	#* <tt>>=</tt> - greater-than-or-equal - (<tt><a,b> >= <c,d> <=> a>=c and b<=d</tt>)		#:* <tt>>=</tt> : greater-than-or-equal - (<tt><a,b> >= <c,d> <=> a>=c and b<=d</tt>)
	#* <tt><=</tt> - less-than-or-equal		#:* <tt><=</tt> : less-than-or-equal
	#: All operators should be surrounded with spaces.		#: All operators should be surrounded with spaces.
	#: Example file:		#: Example file:
Line 88:		Line 88:
	# Set shots to be '''5''' or more.		# Set shots to be '''5''' or more.
	# Click '''“Draw graph for the relation “less than or equal””'''. This may take some time.		# Click '''“Draw graph for the relation “less than or equal””'''. This may take some time.
	# By default, a transitive reduction is applied, since the relation < is transitive. If i1 < i2 and i2 < i3, the corresponding ribs are colored in black and the rib from i1 to i3 is colored in gray.		# By default, a transitive reduction is applied, since the relation < is transitive. If <tt>i1 < i2 and i2 < i3</tt>, the corresponding ribs are colored in black and the rib from <tt>i1</tt> to <tt>i3</tt> is colored in gray.

	== Algorithm ==		== Algorithm ==
Line 94:		Line 94:
	IFSTool uses binary trees to represent the expressions.		IFSTool uses binary trees to represent the expressions.
	When a formula has to be checked:		When a formula has to be checked:
	# The formula is optimized as much as possible. For example, a*(b-b) is equivalent to 0. Many IF-specific optimizations are performed.		# The formula is optimized as much as possible. For example, <tt>a*(b-b)</tt> is equivalent to <tt>0</tt>. Many IF-specific optimizations are performed.
	# The formula is checked in several values. For example, if the step is 0.5 (3 shots in the interval [0, 1]), the following values are used: <0,0>, <0,0.5>, <0,1>, <0.5,0>, <0.5,0.5>, <1,0>. If the formula is not satisfied on any of the values, it is marked as “not satisfied” and no further checks are made for it.		# The formula is checked in several values. For example, if the step is 0.5 (3 shots in the interval [0, 1]), the following values are used: <0,0>, <0,0.5>, <0,1>, <0.5,0>, <0.5,0.5>, <1,0>. If the formula is not satisfied on any of the values, it is marked as '''“not satisfied”''' and no further checks are made for it.
	# The formula is attempted to be proved by checking a large set of rules. For example, if max(x,y)>z has to be proved, it is replaced by the disjunction (x>z \| y>z).		# The formula is attempted to be proved by checking a large set of rules. For example, if <tt>max(x,y)>z</tt> has to be proved, it is replaced by the disjunction <tt>(x>z \| y>z)</tt>.

	[[Category:Intuitionistic fuzzy sets]]		[[Category:Intuitionistic fuzzy sets]]
	[[Category:Software]]		[[Category:Software]]

← Older revision		Revision as of 18:20, 18 July 2010
Line 1:		Line 1:
	'''IFSTool''' is a software for checking properties of [[intuitionistic fuzzy implications]] and [[intuitionistic fuzzy negations\|negations]]. It is being developed by [[Dimitar Dimitrov]] in the frames of the bilateral scientific exchange project [[Ifigenia:Design and development of intuitionistic fuzzy logic tools in information technologies\|Design and development of intuitionistic fuzzy logic tools in information technologies]]. IFSTool requires Microsoft .NET Framework (already installed on newer MS Windows versions) to run.		'''IFSTool''' is a software for checking properties of [[intuitionistic fuzzy implications]] and [[intuitionistic fuzzy negations\|negations]]. It is being developed by [[Dimitar Dimitrov]] in the frames of the bilateral scientific exchange project [[Ifigenia:Design and development of intuitionistic fuzzy logic tools in information technologies\|Design and development of intuitionistic fuzzy logic tools in information technologies]]. IFSTool requires Microsoft .NET Framework (already installed on newer MS Windows versions) to run.

			== Basic properties ==

	Some of the properties that can be checked are the following:		Some of the properties that can be checked are the following:
Line 19:		Line 21:
	: <tt>2: 1-sg(a-c), d*sg(a-c)</tt>		: <tt>2: 1-sg(a-c), d*sg(a-c)</tt>

	== Checking the validity of user-defined axioms ==		=== Checking the validity of user-defined axioms ===

	To check the validity of axioms for a set of implications (or negations), you have to execute the following steps:		To check the validity of axioms for a set of implications (or negations), you have to execute the following steps:
	# Click '''"Import from File"''' to load a text file with implications or negations. Several files can be imported and appended.		# Click '''"Import from File"''' to load a text file with implications or negations. Several files can be imported and appended.
Line 56:		Line 59:
	# By default, each axiom is tested with all implications and their corresponding negations. If '''"Use only corresponding negations"''' is unchecked, all axioms will be checked for all combinations of implications and negations.		# By default, each axiom is tested with all implications and their corresponding negations. If '''"Use only corresponding negations"''' is unchecked, all axioms will be checked for all combinations of implications and negations.

	== Removal of duplicate operations ==		=== Removal of duplicate operations ===

	To remove duplicate implications (or negations, respectively):		To remove duplicate implications (or negations, respectively):
Line 71:		Line 74:
	# If the new implication/negation is equivalent to some old one, this could be seen in the report window.		# If the new implication/negation is equivalent to some old one, this could be seen in the report window.

	== Drawing the graph of relations ==		=== Drawing the graph of relations ===

	To draw a graph for the relation <tt><</tt> :		To draw a graph for the relation <tt><</tt> :