
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/*.
Quantified Resolution Proof, Automated Reasoning, Generalized Axioms
Quantified Resolution Proof, Automated Reasoning, Generalized Axioms
| 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 |
