Prime Implicate Generation in Equational Logic
Authors: Mnacho Echenim, Nicolas Peltier, Sophie Tourret
JAIR 2017 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Finally, an experimental evaluation of this prime implicate generation method is conducted in the ground case, including a comparison with state-of-the-art propositional and first-order prime implicate generation tools. |
| Researcher Affiliation | Academia | Mnacho Echenim EMAIL Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000 Grenoble France, Nicolas Peltier EMAIL Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000 Grenoble France, Sophie Tourret EMAIL Max-Planck-Institut f ur Informatik, Saarland Informatics Campus, Campus E1 4, 66123 Saarbr ucken, Germany |
| Pseudocode | Yes | The paper contains "Algorithm 1 is Included(X, T)", "Algorithm 2 is Entailed([C |X], T, M, N)", "Algorithm 3 prune Included(X, T)", "Algorithm 4 prune Inf([C |X], T, N)", and "Algorithm 5 prune Entailed([C |X], T, M, N)" which are clearly labeled algorithm blocks. |
| Open Source Code | Yes | Our prime implicate generation method has been implemented in a research prototype written in OCaml7. The system, called c SP, is available at https://forge.imag.fr/docman/ ?group_id=683. |
| Open Datasets | Yes | We thus created our own benchmark, made of a thousand randomly generated formulæ of 6 clauses build on 8 constants and containing between 1 and 5 literals (even such small formulæ can have very large set of prime implicates). ... These benchmarks are included in the archive containing the source code of c SP. |
| Dataset Splits | No | The paper uses sets of randomly generated formulas and problems from the SMT-LIB database as benchmarks for evaluating the performance of their system, but it does not describe any specific training/test/validation splits for these logical problems. The research is focused on logical reasoning and theorem proving, where evaluation typically involves solving sets of problems rather than training models on data splits. |
| Hardware Specification | Yes | All of the experiments were run on a machine equipped with an Intel core i5-3470 CPU and 4 2 GB of RAM running Ubuntu 14.04. |
| Software Dependencies | No | Our prime implicate generation method has been implemented in a research prototype written in OCaml. The system for non-flat clauses is based on the Log Tk library (Cruanes, 2014) for the handling of term ordering and congruence closure. While OCaml and the Log Tk library are mentioned, specific version numbers for these software components are not provided. |
| Experiment Setup | Yes | The order in which the c-clauses are processed is fixed by comparing the size of the constraints and of the clausal parts, in lexicographic increasing order. |