Satallax: An automatic higher-order prover. Brown, C. E. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), volume 7364 LNAI, pages 111--117, 2012.
doi  abstract   bibtex   
Satallax is an automatic higher-order theorem prover that generates propositional clauses encoding (ground) tableau rules and uses MiniSat to test for unsatisfiability. We describe the implementation, focusing on flags that control search and examples that illustrate how the search proceeds.
@inproceedings{Brown2012,
abstract = {Satallax is an automatic higher-order theorem prover that generates propositional clauses encoding (ground) tableau rules and uses MiniSat to test for unsatisfiability. We describe the implementation, focusing on flags that control search and examples that illustrate how the search proceeds.},
author = {Brown, Chad E.},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
doi = {10.1007/978-3-642-31365-3_11},
isbn = {9783642313646},
issn = {03029743},
keywords = {higher-order logic,higher-order theorem proving,simple type theory},
pages = {111--117},
title = {{Satallax: An automatic higher-order prover}},
volume = {7364 LNAI},
year = {2012}
}

Downloads: 0