An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic
Authors: Camillo Fiorentini
IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | 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) }. |