[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

In recent years some papers have addressed the problem of the validity in Intuitionistic Propositional Logic (IPL) using the approach proposed by Claessen and Rosén based on reduction to Satisfiability Modulo Theories. This approach depends on an initial preprocessing phase that reduces the input formula in the intuitionistic language to an equivalent sequent in the language of clauses. In this paper we present general clauses, an extension of the clauses used by Claessen and Rosén, that allow us to define a natural relationship between the semantics of the extended clauses and Kripke semantics. We present a decision procedure for general clauses and we show how to encode intuitionistic formulas in the language of general clauses so to decide IPL. The experimental results show that our implementation in general outperforms the state-of-the-art provers for IPL. In principle general clauses can be used as a target language for other non-classical logics with Kripke semantics, so that our decision procedure can be used to decide them.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. \(\texttt{intuitRGC}\) can be downloaded at https://github.com/cfiorentini/intuitRGC.

  2. Typically, a clause is defined as a disjunction of literals, which can be represented as a set of literals. However, following [14], we directly define a clause as a set of literals to streamline certain details.

  3. Redundant lines are omitted, e.g. self-loops, the line connecting \(w_0\) with \(w_3\).

  4. Available at https://github.com/cfiorentini/intuitRGC.

  5. We have adjusted Claessen and Rosén original intuit implementation in order to print additional information. In intuit, classical and non-classical clauses are called flat and implication clauses respectively.

References

  1. Chagrov, A.V., Zakharyaschev, M.: Modal Logic. Oxford Logic Guides, vol. 35. Oxford University Press, Oxford (1997)

    Book  Google Scholar 

  2. Claessen, K., Rosén, D.: SAT modulo intuitionistic implications. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20. LNCS, vol. 9450, pp. 622–637. Springer, Cham (2015). https://doi.org/10.1007/978-3-662-48899-7_43

    Chapter  Google Scholar 

  3. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44(1), 36–50 (1979). https://doi.org/10.2307/2273702

    Article  MathSciNet  Google Scholar 

  4. Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symbolic Logic 57(3), 795–807 (1992). https://doi.org/10.2307/2275431

    Article  MathSciNet  Google Scholar 

  5. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference, SAT. LNCS, vol. 2919, pp. 502–518. Springer, Cham (2003). https://doi.org/10.1007/978-3-540-24605-3_37

    Chapter  Google Scholar 

  6. Ferrari, M., Fiorentini, C., Fiorino, G.: fCube: an efficient prover for intuitionistic propositional logic. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 294–301. Springer, Cham (2010). https://doi.org/10.1007/978-3-642-16242-8_21

    Chapter  Google Scholar 

  7. Ferrari, M., Fiorentini, C., Fiorino, G.: Simplification rules for intuitionistic propositional tableaux. Trans. Comput. Logic 13(2), 14–11423 (2012). https://doi.org/10.1145/2159531.2159536

    Article  MathSciNet  Google Scholar 

  8. Ferrari, M., Fiorentini, C., Fiorino, G.: Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models. J. Autom. Reason. 51(2), 129–149 (2013). https://doi.org/10.1007/s10817-012-9252-7

    Article  MathSciNet  Google Scholar 

  9. Fiorentini, C., Ferrari, M.: SAT-based proof search in intermediate propositional logics. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) Automated Reasoning—11th International Joint Conference, IJCAR. LNCS, vol. 13385, pp. 57–74. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-10769-6_5

  10. Fiorentini, C.: An ASP approach to generate minimal countermodels in intuitionistic propositional logic. In: Kraus, S. (eds.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI, pp. 1675–1681 (2019). https://doi.org/10.24963/ijcai.2019/232

  11. Fiorentini, C.: Efficient SAT-based proof search in intuitionistic propositional logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE 28. LNCS, vol. 12699, pp. 217–233. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_13

    Chapter  Google Scholar 

  12. Fiorentini, C., Ferrari, M.: Duality between unprovability and provability in forward refutation-search for intuitionistic propositional logic. ACM Trans. Comput. Log. 21(3), 22–12247 (2020). https://doi.org/10.1145/3372299

    Article  MathSciNet  Google Scholar 

  13. Fiorentini, C., Goré, R., Graham-Lengrand, S.: A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS, vol. 11714, pp. 111–129. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29026-9_7

    Chapter  Google Scholar 

  14. Gallier, J.H.: The completeness of propositional resolution: a simple and constructive proof. Log. Methods Comput. Sci. (2006). https://doi.org/10.2168/LMCS-2(5:3)2006

    Article  MathSciNet  Google Scholar 

  15. Goré, R., Kikkert, C.: CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS, vol. 12842, pp. 74–91. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-86059-2_5

    Chapter  Google Scholar 

  16. Goré, R., Thomson, J., Wu, J.: A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 262–268. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_19

    Chapter  Google Scholar 

  17. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL( T). J. ACM 53(6), 937–977 (2006). https://doi.org/10.1145/1217856.1217859

    Article  MathSciNet  Google Scholar 

  18. Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic. J. Autom. Reason. 38(1–3), 261–271 (2007). https://doi.org/10.1007/s10817-006-9060-z

    Article  MathSciNet  Google Scholar 

  19. Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, vol. 43, 2nd edn. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2000). https://doi.org/10.1017/CBO9781139168717

    Book  Google Scholar 

Download references

Acknowledgements

Camillo Fiorentini is member of the Gruppo Nazionale Calcolo Scientifico-Istituto Nazionale di Alta Matematica (GNCS-INdAM).

Author information

Authors and Affiliations

  1. Department of Computer Science, Università degli Studi di Milano, Via Celoria, 18, 20133, Milan, MI, Italy

    Camillo Fiorentini

  2. Department of Theoretical and Applied Sciences, Università degli Studi dell’Insubria, Via J.H. Dunant, 3, 21100, Varese, VA, Italy

    Mauro Ferrari

Authors
  1. Camillo Fiorentini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mauro Ferrari
    View author publications

    You can also search for this author in PubMed Google Scholar

Contributions

The authors have contributed equally to this article.

Corresponding authors

Correspondence to Camillo Fiorentini or Mauro Ferrari.

Ethics declarations

Competing interests

The authors declare no competing interests.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Fiorentini, C., Ferrari, M. General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic. J Autom Reasoning 68, 13 (2024). https://doi.org/10.1007/s10817-024-09703-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s10817-024-09703-8

Keywords

Mathematics Subject Classification

Search

Navigation