Quick Start
FST Instructions and Usage
To start you must call the program. To do so you can use open in any browser the URL http://fst.educa.pt .
The screen shows the login screen (see fig. A.1). a classical IDE with fields to enter Login and Password and a toolbar on top.
Figure A.1: Open Screen
As you see in the figure you must enter a valid Login user and the corresponding password. If you do not have a login you have two choices: first, create a new one by selecting the option “Don’t have a Login? Click here For Register.” .The second option is to enter as Guest, and you will have all functionalities as an normal user. The difference is that your work will not be saved.
Figure A.2: Register Login
When you login the system will provide the last jobs you did on your account.
Figure A.3: Login
Figure A.4: Main Screen
On top of the interface you have the options: “Upload File”, “Initialize the System” and “Exit” :
Option Upload File - This option allows the user to upload a file in Prover9 syntax to be used in the FST.
Figure A.5: Upload File
Option Initialize the System – This option refresh all boxes Axioms, Pivot, Configuration and Results. Also provides a default pair of conjectures.
Figure A.6: Initilizate the System
This option afects all inputs, they assume default values, so we have:
Figure A.7: System Default - Initialized
In the tab Configuration we have by default the following values:
Max Time:60
Number Models:1
Domain Start:2
Domain End:6
For Axioms:
(x * y) * z = x * (y * z).
x * x = x.
x * ( y * x ) = x.
For Pivot
x * y = x.
In order to start using the program, the user must select the intended procedure. There are two of them: Normal or Extended. By default, the Normal tab is selected, which has two buttons, "Generate Forbidden Substructure" and "Generate Forbidden Substructure Theorems". Let us see how each one works:
- "Generate Forbidden Substructure" performs the procedure of finding the Number Models of the orders specified in Domain Start and Domain End.
So if we select the button "Generate Forbidden Substructure", with the default values for Axioms and Pivot specified above it processes the data, and we get the results in the tab RESULTS:
This option afects all inputs, they assume default values, so we have:
Figure A.8: Results - Generate Forbidden Substructure
---------------
Model Class 2
----------------
interpretation( 2, [number = 1,seconds = 0], [
function(*(_,_), [
0,1,
0,1]),
function(c1, [0]),
function(c2, [1])]).
----------------
Mace Fail
-------Failure----Dom 2-----
Mace Fail
-------Failure----Dom 3-----
Mace Fail
-------Failure----Dom 4-----
Mace Fail
-------Failure----Dom 5-----
Mace Fail
-------Failure----Dom 6-----
Success
The system gives all the forbidden models found under the given constraints.
- "Generate Forbidden Substructure Theorems" searches for one model at a time starting from the lowest order specified and, whenever a model is found, tries to prove a forbidden substructure theorem. If it finds a counterexample, the new model is used to find a theorem, and so it goes.
Therefore, if we select the button "Generate Forbidden Substructure Theorems", with the default values for Axioms and Pivot, it processes the data, and we get the results in the tab RESULTS: This option uses all inputs with the default values, so we have:
Figure A.9: Results - Generate Forbidden Substructure Theorems
---------------
Model found
----------------
interpretation( 2, [number = 1,seconds = 0], [
function(*(_,_), [
0,1,
0,1]),
function(c1, [0]),
function(c2, [1])]).
THEOREM
----------------
An algebra satisfies
(x * y) * z = x * (y * z).
x * x = x.
x * ( y * x ) = x.
x * y = x.
iff it satisfies
(x * y) * z = x * (y * z).
x * x = x.
x * ( y * x ) = x.
and does not contain
interpretation( 2, [number = 1,seconds = 0], [
function(*(_,_), [
0,1,
0,1]),
function(c1, [0]),
function(c2, [1])]).
The proof of this theorem can be obtained using ProverX (www.proverx.com) with the following input
assign(max_seconds, 60).
formulas(assumptions).
(x * y) * z = x * (y * z).
x * x = x.
x * ( y * x ) = x.
exists x exists y -(x * y = x).
end_of_list.
formulas(goals).
exists a0 exists a1 (a0 != a1 & *(a0,a1) = a1
).
end_of_list.
Or with this alternative input
Assumptions:
(x * y) * z = x * (y * z).
x * x = x.
x * ( y * x ) = x.
x * y != x.
(x0 = x1 | *(x0,x1) != x1 ).
"Theory" To get this option, you must select underneath the main menu the option Extended, and you get a tab with that name. This option takes a group of axioms that define a Theory and tries to find sequences of theorems based in the combination of the axioms of the Theory. The method is sequential, it combines Axioms and Pivot to find Forbidden Substructure Theorems. When it finds one discards the Pivot and makes a new combination with the rest of the axioms and so on.
The configuration relevant for this operation is the max time specified, and the order given in Max Time and Domain Start.
Figure A.10: Theories Search
