Automated Generation of Consistent Graph Models with Theorem Provers - ArenBabikian/publication-pages GitHub Wiki

Reference

This is the publication page for:

@inproceedings {TPTPGraphGeneration,
	author = {Aren Babikian and Oszk{\'a}r Semer{\'a}th and D{\'a}niel Varr{\'o}}
	title = {Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers},
	booktitle = {23rd International Conference on Fundamental Approaches to Software Engineering (FASE 2020)},
	year = {2020},
	month = {4}
}

Implementation

The implementation of my research is done on the Vampire-ArenB branch of the VIATRA Model Generator project. I plan on integrating my work into the master branch of the repository within the near future.

Sample TPTP files used to generate models of various sizes (specified in the file names) are gathered here. These files are generated automatically as described in our paper.

Running the Theorem Provers

TPTP-compliant theorem provers can be run on our generated TPTP files through the System on TPTP web interface. Users must add the generated TPTP file as the input problem, select the desired output mode and select the desired theorem provers to run. Users must then run the selected systems (by clicking on the "RunSelectedSystems" button) to obtain the theorem prover outputs.

Theorem Prover Outputs

Sample outputs from various theorem provers at different model size specifications are gathered here. These files contain the required details regarding the model generated by the theorem prover.

Evaluation Results

Our complete evaluation results are available here. The Excel file also contains all results-related figures found in the paper.