CoChat
Sign Up
Cited by 3Logic, Reasoning, and KnowledgeLogic, programming, and type systemsComputability, Logic, AI Algorithms

SLD-Resolution Reduction of Second-Order Horn Fragments

Open access
Tourret, Sophie, Cropper, Andrew·2019·Lecture Notes in Computer Science
DOI 10.1007/978-3-030-19570-0_17
Open this paper in CoChat — free accountOpen PDF

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1007/978-3-030-19570-0_17

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • There is preliminary work in reasoning about metarules to identify universal sets suitable to learn certain fragments of logic programs.

    “For this reason, there is preliminary work in reasoning about metarules to identify universal sets suitable to learn certain fragments of logic programs (Cropper & Muggleton, 2014; Tourret & Cropper, 2019; Cropper & Tourret, 2020).”

    From Inductive Logic Programming At 30: A New Introduction (2022) · cites this paper as Tourret & Cropper, 2019

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

The citation lists haven’t been fetched yet

References 54 · Cited by 3

Research works printed but not linked: 42

  1. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017)
  2. Bienvenu, M.: Prime implicates and prime implicants in modal logic. In: Proceedings of the National Conference on Artificial Intelligence. vol. 22, p. 379. Menlo Park, CA; Cambridge, MA; London; AAAI Press; MIT Press (2007)
  3. Buntine, W.: Generalized subsumption and its applications to induction and redundancy. Artificial intelligence 36(2), 149-176 (1988). https://doi.org/10.1016/0004-3702(88)90001-X · DOI · Paper page
  4. Campero, A., Pareja, A., Klinger, T., Tenenbaum, J., Riedel, S.: Logical Rule Induction and Theory Learning Using Neural Theorem Proving. ArXiv e-prints (Sep 2018)
  5. Charalambidis, A., Handjopoulos, K., Rondogiannis, P., Wadge, W.W.: Extensional higher-order logic programming. ACM Trans. Comput. Log. 14(3), 21:1-21:40 (2013). https://doi.org/10.1145/2499937.2499942 · DOI
  6. Cropper, A.: Efficiently learning efficient programs. Ph.D. thesis, Imperial College London, UK (2017)
  7. Cropper, A., Muggleton, S.H.: Logical minimisation of meta-rules within meta-interpretive learning. In: Davis, J., Ramon, J. (eds.) Inductive Logic Programming -24th International Con- ference, ILP 2014, Revised Selected Papers. Lecture Notes in Computer Science, vol. 9046, pp. 62-75. Springer (2014). https://doi.org/10.1007/978-3-319-23708-4 5 · DOI
  8. Cropper, A., Muggleton, S.H.: Learning higher-order logic programs through abstraction and invention. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016. pp. 1418-1424. IJCAI/AAAI Press (2016)
  9. Cropper, A., Tourret, S.: Derivation reduction of metarules in meta-interpretive learning. In: Inductive Logic Programming -28th International Conference, ILP 2018, Ferrara, Italy, September 2-4, 2018, Proceedings. pp. 1-21 (2018). https://doi.org/10.1007/978-3-319-99960- 9 1 · DOI
  10. Dantsin, E., Eiter, T., Gottlob, G., Voronkov, A.: Complexity and expressive power of logic programming. ACM Comput. Surv. 33(3), 374-425 (2001). https://doi.org/10.1145/502807.502810 · DOI · Paper page
  11. Dirac, G.A.: Some theorems on abstract graphs (1952). https://doi.org/10.1112/plms/s3-2.1.69 · DOI
  12. Echenim, M., Peltier, N., Tourret, S.: Quantifier-free equational logic and prime implicate generation. In: CADE-25. pp. 311-325. Springer (2015)
  13. Evans, R., Grefenstette, E.: Learning explanatory rules from noisy data. J. Artif. Intell. Res. 61, 1-64 (2018). https://doi.org/10.1613/jair.5714 · DOI · Paper page
  14. Gottlob, G., Fermüller, C.G.: Removing redundancy from a clause. Artificial Intelligence 61(2), 263-289 (1993)
  15. Grädel, E.: The expressive power of second order horn logic. In: STACS 91, 8th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings. pp. 466-477 (1991). https://doi.org/10.1007/BFb0020821 · DOI
  16. Hemaspaandra, E., Schnoor, H.: Minimization for generalized boolean formulas. In: IJCAI Proceedings-International Joint Conference on Artificial Intelligence. vol. 22, p. 566 (2011)
  17. Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. Journal of Artificial Intelligence Research 53, 127-168 (2015)
  18. Hillenbrand, T., Piskac, R., Waldmann, U., Weidenbach, C.: From search to computation: Redundancy criteria and simplification at work. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics -Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science, vol. 7797, pp. 169-193. Springer (2013). https://doi.org/10.1007/978-3-642-37651- 1 7 · DOI
  19. Hohenecker, P., Lukasiewicz, T.: Deep learning for ontology reasoning. CoRR abs/1705.10342 (2017) · arXiv
  20. Huet, G.P.: A mechanization of type theory. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence. pp. 139-146 (1973)
  21. Immerman, N.: Descriptive complexity. Springer Science & Business Media (2012)
  22. Joyner Jr., W.H.: Resolution strategies as decision procedures. J. ACM 23(3), 398-417 (1976). https://doi.org/10.1145/321958.321960 · DOI
  23. Kaminski, T., Eiter, T., Inoue, K.: Exploiting answer set programming with external sources for meta-interpretive learning. In: 34th International Conference on Logic Programming (2018)
  24. Kowalski, R.A.: Predicate logic as programming language. In: IFIP Congress. pp. 569-574 (1974)
  25. Langlois, M., Mubayi, D., Sloan, R., Turán, G.: Combinatorial problems for Horn clauses. Graph Theory, Computational Intelligence and Thought pp. 54-65 (2009)
  26. Liberatore, P.: Redundancy in logic I: CNF propositional formulae. Artif. Intell. 163(2), 203-232 (2005). https://doi.org/10.1016/j.artint.2004.11.002 · DOI
  27. Liberatore, P.: Redundancy in logic II: 2CNF and Horn propositional formulae. Artif. Intell. 172(2-3), 265-299 (2008). https://doi.org/10.1016/j.artint.2007.06.003 · DOI
  28. Marquis, P.: Consequence finding algorithms. In: Handbook of Defeasible Reasoning and Uncertainty Management Systems, pp. 41-145. Springer (2000)
  29. McCarthy, J.: Making robots conscious of their mental states. In: Machine Intelligence 15, Intelligent Agents [St. Catherine's College, Oxford, July 1995]. pp. 3-17 (1995)
  30. Muggleton, S.: Inductive Logic Programming. New Generation Computing 8(4), 295-318 (1991)
  31. Muggleton, S., Raedt, L.D., Poole, D., Bratko, I., Flach, P.A., Inoue, K., Srinivasan, A.: ILP turns 20 -biography and future challenges. Machine Learning 86(1), 3-23 (2012). https://doi.org/10.1007/s10994-011-5259-2 · DOI · Paper page
  32. Nienhuys-Cheng, S.H., Wolf, R.d.: Foundations of Inductive Logic Programming. Springer- Verlag New York, Inc., Secaucus, NJ, USA (1997)
  33. Plotkin, G.: Automatic Methods of Inductive Inference. Ph.D. thesis, Edinburgh University (August 1971)
  34. Raedt, L.D.: Declarative modeling for machine learning and data mining. In: Algorith- mic Learning Theory -23rd International Conference, ALT, Proceedings. p. 12 (2012). https://doi.org/10.1007/978-3-642-34106-9 2 · DOI
  35. Raedt, L.D., Bruynooghe, M.: Interactive concept-learning and constructive induction by analogy. Machine Learning 8, 107-150 (1992). https://doi.org/10.1007/BF00992861 · DOI
  36. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23-41 (1965). https://doi.org/10.1145/321250.321253 · DOI
  37. Rocktäschel, T., Riedel, S.: End-to-end differentiable proving. In: Guyon, I., von Luxburg, U., Bengio, S., Wallach, H.M., Fergus, R., Vishwanathan, S.V.N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017. pp. 3791-3803 (2017)
  38. Sato, T.: Equivalence-preserving first-order unfold/fold transformation systems. Theor. Com- put. Sci. 105(1), 57-84 (1992). https://doi.org/10.1016/0304-3975(92)90287-P · DOI
  39. Si, X., Lee, W., Zhang, R., Albarghouthi, A., Koutris, P., Naik, M.: Syntax-guided synthesis of datalog programs. In: Leavens, G.T., Garcia, A., Pasareanu, C.S. (eds.) Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018. pp. 515-527. ACM (2018). https://doi.org/10.1145/3236024.3236034 · DOI
  40. Tärnlund, S.: Horn clause computability. BIT 17(2), 215-226 (1977)
  41. Tourret, S., Cropper, A.: SLD-resolution reduction of second-order Horn fragments. Tech. rep., https://arxiv.org/abs/1902.09900 (2018) · arXiv
  42. Weidenbach, C., Wischnewski, P.: Subterm contextual rewriting. AI Commun. 23(2-3), 97- 109 (2010). https://doi.org/10.3233/AIC-2010-0459 A Omitted Proofs from Section 5 (Prop. 12) The proofs in this section assume that in a clause (1) no two literals share more than one variable, and (2) no predicate variable occurs more than once. Condition (1) allows us · DOI

Authors
Tourret, S., & Cropper, A.
Affiliations
  • Max Planck Institute for Informatics (DE)
  • University of Oxford (GB)
Corresponding author
Tourret, Sophie
ORCID
Venue
Lecture Notes in Computer Science
Publisher
Springer International Publishing
Published
2019
Pages
259-276
ISSN
  • 0302-9743 (ISSN-L)
  • 1611-3349
DOI
10.1007/978-3-030-19570-0_17
OpenAlex
W2922022659
Cited by
3
References
54
Citations by year
2025: 1 · 2022: 1 · 2019: 1
FWCI
0.19
Type
conference paper
Language
en
Open access
Licence
Locations
  • Lecture notes in computer science (publishedVersion)
  • HAL (submittedVersion, other-oa)
  • Oxford University Research Archive (ORA) (University of Oxford) (submittedVersion)
  • MPG.PuRe (Max Planck Society) (submittedVersion)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Computability, Logic, AI Algorithms
Keywords
SLD-resolution, inductive logic programming, logic programming, undecidability

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review