| Home | Grammar | Facts | Reasoning | Knowledge base | Software | Download |
The Verish program is provided as source code written in ANSI C++. On a Linux system, with the program files Verish.cpp, Verish.h, and VUtils.cpp in the current directory, it can be built, for example, with the command:
g++ -o Verish Verish.cpp VUtils.cpp -Wall
This will put the executable Verish program in the current directory. The reasoning in a file in the current directory named, for example, kb.ver, can now be checked with the command:
./Verish kb.ver
This will output the Sentences in the file, each followed by a message such as Title, Abbreviation, Definition, Method, Reason, or Fact, until either the end of the file is reached, or an error is encountered, in which case the program outputs an error message and then stops.
In addition to its basic function as above, the program can perform several other functions to facilitate the development of proofs in Verish, and the presentation of proofs in structured pages as in the knowledge base on this website. The utility functions are invoked by including options in the command line after the name of the input file. The currently available utility functions are invoked as in the following examples, shown for an input file called kb.ver.
./Verish kb.ver -addMthApps
will add the Applications of the currently implemented automatic Methods. The output is sent to standard output, usually the console, and the input file, here kb.ver, is not altered. The output can be redirected to a required output file, for example kbAp.ver, as in the following example:
./Verish kb.ver -addMthApps > kbAp.ver
The html markup to present the proofs in a file in a structured page as in the knowledge base on this website can be added as in the following example.
./Verish kb.ver -addhtmlmkup vtop vbot
Here vtop and vbot are files that are added at the start and end of the output. vtop should contain the Javascript fragment found at the start of the <body> section of the knowledge base pages. The output is again sent to standard output, and the input file, here kb.ver, is not altered. The output can be redirected to a required output file, for example kbH.ver, as in the following example:
./Verish kb.ver -addhtmlmkup vtop vbot > kbAp.ver
The source code is structured so that the basic reasoning checking function is carried out by the code in Verish.cpp, so that if you just want to check that the program will detect all errors of reasoning, you only need to check the source code in that file. The code in Verish.cpp is intended to evolve towards a stable state.
The utility functions are coded in VUtils.cpp, and the code in VUtils.cpp is intended to grow steadily with time, as new automatic Methods and utility functions are added. The functions in Verish.cpp are made available in the Verish.h header file, which is included in VUtils.cpp, but with the exception of the function VUtilsMain( ... ), which is declared in Verish.h, none of the functions in VUtils.cpp, and any additional utility files added later, will be used or included in Verish.cpp, even if they are eventually made available in header files.
The current version of the Verish program is Verish 0.95. It has the following known issues, which will be resolved as rapidly as practical.
The English and Verish text on this website is licensed for use under the Free Software Foundation Free Documentation License, and the software is licensed for use under the Free Software Foundation General Public License.
Page last updated 25 May 2018. Copyright (c) Chris Austin 1997 - 2018. Privacy policy