Expressive Logical Combinators for Free
Authors: Pierre Geneves, Alan Schmitt
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We report on practical applications in 4 with experimental results that illustrate that the lean size is indeed a better indicator of the problem s complexity than formula size. The satisfiability check of the above formula is performed in 131ms (milliseconds) with the implementation [Genev es et al., 2015b], including 5ms for computing the lean and 104ms for computing the tableau. A sample satisfying tree of 33 nodes is also constructed in 39ms. |
| Researcher Affiliation | Academia | Pierre Genev es CNRS, LIG Alan Schmitt Inria, Rennes Detailed affiliation of authors: P. Genev es (CNRS, Laboratoire d Informatique de Grenoble, Inria, Univ. Grenoble Alpes) and A. Schmitt (Inria, Research Center Rennes Bretagne Atlantique). |
| Pseudocode | No | The paper includes formal definitions of lean (Figure 1) and recursive expansions (Figure 2), which are mathematical notations, but not pseudocode or algorithm blocks describing a computational procedure. |
| Open Source Code | Yes | We provide an implementation of the proposed system [Genev es et al., 2015b]. Each example given in this section comes in a boxed version that can directly be used with the implementation [Genev es et al., 2015b]. Tests are thus reproducible. The XML reasoning project: http://wam.inrialpes.fr/websolver/ |
| Open Datasets | No | The paper describes examples and computations on formulas, constructing "sample satisfying tree[s]" for these formulas. However, it does not mention using or training on any publicly available dataset or provide access information for a dataset. |
| Dataset Splits | No | The paper does not provide information about training/test/validation dataset splits or cross-validation. It focuses on the computational complexity of logical formulas and their satisfaction. |
| Hardware Specification | No | The paper mentions computation times in milliseconds but does not specify any hardware details like CPU, GPU, or memory used for the experiments. |
| Software Dependencies | No | The paper mentions using "an off-the-shelf satisfiability solver" and refers to their own "implementation [Genev es et al., 2015b]", but it does not specify version numbers for any software components or libraries, such as programming languages, operating systems, or specific solver versions. |
| Experiment Setup | Yes | The paper describes the specific logical formulas and combinators used as input for the experiments (e.g., 'split(split(split(ϕ)))', 'psi() & next(psi() & next(psi() & next(psi())))'). It also details the size characteristics of these formulas in terms of atomic propositions, modalities, conjunctions, and disjunctions, and the corresponding lean sizes (e.g., 'ψ contains 24 atomic propositions, 38 modalities...', 'The size of the lean is only 19'). This constitutes the setup for their logical experiments. |