Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
versions View all 2 versions
addClaim

QRP+Gen: Checking Q-Resolution Proofs with Generalized Axioms

Authors: Peyrer, Mark; Seidl, Martina;

QRP+Gen: Checking Q-Resolution Proofs with Generalized Axioms

Abstract

QRP+Gen: Checking Q-Resolution Proofs with Generalized Axioms This is the artifact for QRP+Gen, a new proof-system extending Q-resolution with generalized Axioms. It was submitted as additional material to the corresponding paper submitted to the SAT25 and made publically available here. The artifact contains everything necessary for setting up and running the QRP+Gen pipeline. In order to build, call ./configure.sh and all necessary sources will be compiled. The script ./run.sh can be parameterized with a *.qdimacs-formula to solve and check it, i.e. using the full pipeline. In order to just execute individual steps, ./solve.sh and ./check.sh can be used.Note that for checking, it is necessary to have drat-tim and the novel trivial-truth checker ttcheck in the same folder thus we recommend running the test with the current directory as working directory as the configure script will ensure the presence of all necessary executables. In the samples folder, three very simple formulas to be checked can be found. One of them (tf_parity_multiplex20.qdimacs) is a medium-sized crafted formula following the structure described in our paper (n=20).If additional crafted formulas have to be produced, please use our generator found in crafted/tf_parity_multiplex.py (python3 is required) The following third party tools are included in this artifact: DepQBF (with modifications) CaDiCaL drat-tim QRPcheck (with modifications) The licences of this tools may be found in the corresponding source-directories in src/*.

Related Organizations
Keywords

Quantified Resolution Proof, Automated Reasoning, Generalized Axioms

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
0
Average
Average
Average