Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic
Authors: Camillo Fiorentini
IJCAI 2019 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Tests were conducted on a standard machine with a 3.0GHz Intel Core(TM)2 Duo CPU and 3.5GB memory |
| Researcher Affiliation | Academia | Camillo Fiorentini Department of Computer Science, University of Milan, Italy fiorentini@di.unimi.it |
| Pseudocode | Yes | We describe an ASP program ΠG to generate a minimal countermodel for a goal formula G. [...] We present the relevant sections of the program; we assume that G is the goal formula and N = |At(G)|. [...] Example 4 The formula T in Fig. 1 has 7 atomic subformulas, thus A = {a(0), . . . , a(6)}. We set (7 represents ψ ): [...] This is translated by the following ground facts: count_atms(7). at_to_PV(a(0),p). def(a(1),neg(a(0))). [...] { root(W) : pworld(W), not belongs_Clos_G(G,W) } = 1 :-goal(G). [...] #minimize { M : count_Worlds(M) }. |
| Open Source Code | No | The implementation is available at author s home page. This is a general statement that does not provide a specific, direct link to a code repository for the methodology described. |
| Open Datasets | Yes | We have also performed some experiments on the non-valid formulas of Intuitionistic Logic Theorem Proving (ILTP) Library [Raths et al., 2007]. |
| Dataset Splits | No | The paper uses formulas from a logic theorem proving library but does not describe traditional machine learning-style train/validation/test dataset splits for its experiments. It focuses on generating countermodels rather than training models on data. |
| Hardware Specification | Yes | Tests were conducted on a standard machine with a 3.0GHz Intel Core(TM)2 Duo CPU and 3.5GB memory |
| Software Dependencies | No | We exploit the Potassco tool clingo [Gebser et al., 2011]. While the software `clingo` is mentioned, a specific version number for `clingo` itself is not provided in the text. |
| Experiment Setup | Yes | We describe an ASP program ΠG to generate a minimal countermodel for a goal formula G. [...] Firstly, we have to choose the root of the countermodel, designated by the predicate root/1. To this aim, we introduce the following choice rule (Chr): { root(W) : pworld(W), not belongs_Clos_G(G,W) } = 1 :goal(G). [...] Finally, we instruct the solver to search for solutions minimizing the number of worlds, computed by the predicate count_Worlds/1: #minimize { M : count_Worlds(M) }. |