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
{"_id":"bJ23wG5dmG9RSMfRs","bibbaseid":"brown-satallaxanautomatichigherorderprover-2012","downloads":0,"creationDate":"2017-09-01T03:35:40.534Z","title":"Satallax: An automatic higher-order prover","author_short":["Brown, C. E."],"year":2012,"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/jonaprieto/athena/master/paper/ref.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","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":[{"propositions":[],"lastnames":["Brown"],"firstnames":["Chad","E."],"suffixes":[]}],"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","bibtex":"@inproceedings{Brown2012,\nabstract = {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.},\nauthor = {Brown, Chad E.},\nbooktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},\ndoi = {10.1007/978-3-642-31365-3_11},\nisbn = {9783642313646},\nissn = {03029743},\nkeywords = {higher-order logic,higher-order theorem proving,simple type theory},\npages = {111--117},\ntitle = {{Satallax: An automatic higher-order prover}},\nvolume = {7364 LNAI},\nyear = {2012}\n}\n","author_short":["Brown, C. E."],"key":"Brown2012","id":"Brown2012","bibbaseid":"brown-satallaxanautomatichigherorderprover-2012","role":"author","urls":{},"keyword":["higher-order logic","higher-order theorem proving","simple type theory"],"downloads":0},"search_terms":["satallax","automatic","higher","order","prover","brown"],"keywords":["higher-order logic","higher-order theorem proving","simple type theory"],"authorIDs":[],"dataSources":["8jafqMAWgB7XP4FTZ"]}