English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse
  1. View item / 
  2. Item Summary

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Paper

SAT-Inspired Higher-Order Eliminations

MPS-Authors
/persons/resource/persons183227

Blanchette,  Jasmin
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

arXiv:2208.07775.pdf
(Preprint), 330KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Blanchette, J., & Vukmirović, P. (2022). SAT-Inspired Higher-Order Eliminations. Retrieved from https://arxiv.org/abs/2208.07775.


Cite as: https://hdl.handle.net/21.11116/0000-000B-653C-1
Abstract
We generalize several propositional preprocessing techniques to higher-order
logic, building on existing first-order generalizations. These techniques
eliminate literals, clauses, or predicate symbols from the problem, with the
aim of making it more amenable to automatic proof search. We also introduce a
new technique, which we call quasipure literal elimination, that strictly
subsumes pure literal elimination. The new techniques are implemented in the
Zipperposition theorem prover. Our evaluation shows that they sometimes help
prove problems originating from the TPTP library and Isabelle formalizations.