Symbolic Computation and Artificial Intelligence

RISC and AI Slides
RISC and AI Poster

 

Symbolic computation deals with algorithms on symbolic objects that can be defined as finitary representations of infinite mathematical entities. Its main subareas include

  • computer algebra,
  • computational logic, and
  • automated programming.

Traditionally, symbolic computation and artificial intelligence have a big intersection in the area of computational logic, which includes such core subjects of AI as knowledge representation and reasoning, constraint satisfaction, planning and search. RISC members have been very active in this area, publishing papers at various AI-related venues such as the International Joint Conference on Artificial Intelligence (IJCAI), the International Conference on Knowledge Representation and Reasoning (KR), European Conference on Logics in Artificial Intelligence (JELIA), Artificial Intelligence and Symbolic Computation (AISC), Annals of Mathematics and Artificial Intelligence, and in many others with a more specific focus on reasoning such as, e.g., Journal of Automated Reasoning, ACM Transactions on Computational Logic, International Joint Conference on Automated Reasoning (IJCAR), Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Formal Structures on Computation and Deduction (FSCD), Intelligent Computer Mathematics (CICM), etc. They also gave invited talks, served on many related program committees, and organized various conferences or journal special issues on these topics.

Interestingly, when Bruno Buchberger was founding a new institute of the Johannes Kepler University Linz in 1985, he was considering two options as the main notion in its name: “symbolic computation” or “artificial intelligence”. For reasons described in the paper Automated programming, symbolic computation, machine learning: my personal view, he decided for symbolic computation and the name RISC, but already this fact shows how closely symbolic computation and artificial intelligence have been connected.

Automated programming (yet another subarea of symbolic computation) got a big boost recently with the advancement of new machine learning techniques (a subarea of artificial intelligence). This especially concerns the kind of problems where a precise, complete specification is not possible or not feasible. When such a specification is replaced with a (huge number) of input-output examples, these techniques are able to generate a suitable program/algorithm. The core idea is “learning from examples”, where a general structure is “learned” from the given concrete examples. In various forms, this idea can be encountered in different areas of mathematics and logic, e.g., in the interpolation problem (given points in the plane, find a curve of a given type that goes through those points), the regression problem (given points in the plane, find a straight line that minimizes the distance to all points), the guessing problem (given some elements of a number sequence, find a recurrence that describes the sequence), the anti-unification problem (given logic terms, find a term that is their least general generalization), etc. New theoretical methods of machine learning together with the advancement of computing power and the availability of huge data sets made it possible to apply this idea to problems that were far out of reach up to now.

Symbolic Computation and Machine Learning

This impressive success of machine learning techniques brings both new opportunities and new challenges, which open new ways for artificial intelligence by the interaction of machine learning and symbolic computation. We at RISC are interested in exploring these interactions in various directions: as an application of ML in SC (ML → SC), an application of SC in ML (SC → ML), or a combined approach to solving problems (ML + SC + ···), with some typical cases being the following:

  • using modern machine learning methods in generating hypotheses in symbolic computation research (ML → SC);
  • speeding up computer algebra methods by solving subproblems with verified output of machine learning methods (ML → SC);
  • verifying machine-learned algorithms using symbolic computation methods (SC → ML);
  • generating algorithms from natural language specification using methods from natural language processing, machine learning, and symbolic computation (NLP + ML + SC).

Publications, Talks, Activities

Some of the relevant past publications, talks, and activities of RISC members:

  • Bruno Buchberger. Automated programming, symbolic computation, machine learning: my personal view. Annals of Mathematics and Artificial Intelligence, 91(5): 569-589, 2023.
    DOI: doi.org/10.1007/s10472-023-09894-7
  • David M. Cerna, Temur Kutsia: Anti-Unification and Generalization: A Survey. In: Edith Elkind (ed.), Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, pp. 6563-6573. ijcai.org, 2023.
    DOI: doi.org/10.1007/978-3-031-10769-6\_34
  • Wolfgang Schreiner. Concrete Abstractions: Formalizing and Analyzing Discrete Theories and Algorithms with the RISCAL Model Checker. Texts & Monographs in Symbolic Computation, Springer 2023, ISBN 978-3-031-24933-4.
    DOI: doi.org/10.1007/978-3-031-24934-1
  • Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk. Learning Higher-Order Logic Programs From Failures. In: Luc De Raedt (ed.), Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, pp. 2726-2733. ijcai.org, 2022.
    DOI: doi.org/10.24963/ijcai.2022/378
  • Temur Kutsia and Cleo Pau. A Framework for Approximate Generalization in Quantitative Theories. In: Jasmin Blanchette, Laura Kovács, and Dirk Pattinson (eds), Proceedings of 11th International Joint Conference on Automated Reasoning, IJCAR 2022. Lecture Notes in Artificial Intelligence 13385, pp. 578-596. Springer, 2022.
    DOI: doi.org/10.1007/978-3-031-10769-6\_34
  • Temur Kutsia. International Joint Conference on Artificial Intelligence: IJCAI 2023, IJCAI 2024. Member of the program committee, survey track.
  • Wolfgang Schreiner. Thinking Programs: Logical Modeling and Reasoning About Languages, Data, Computations, and Executions. Texts & Monographs in Symbolic Computation, Springer 2021, ISBN 978-3-030-80506-7.
    DOI: doi.org/10.1007/978-3-030-80507-4
  • Wolfgang Schreiner. Validating Mathematical Theories and Algorithms with RISCAL. In: Florian Rabe et al. (eds), Intelligent Computer Mathematics, CICM 2018, Lecture Notes in Artificial Intelligence 11006, pp. 248-254. Springer, 2018.
    DOI: doi.org/10.1007/978-3-319-96812-4\_21
  • Bruno Buchberger. Mathematics: Natural Intelligence. Invited talk at the Symposium in Honor of Peter Paule’s 60th Birthday. RISC, May 17, 2018.
  • Boris Konev, Temur Kutsia. Anti-Unification of Concepts in Description Logic EL. In: Chitta Baral, James P. Delgrande, Frank Wolter (eds), Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, pp 227-236. AAAI Press 2016.
  • Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. Satisfiability checking and symbolic computation. ACM Commun. Comput. Algebra 50(4): 145-147, 2016.
    DOI: doi.org/10.1145/3055282.3055285
  • Alexander Baumgartner, Temur Kutsia. A library of anti-unification algorithms. In: Eduardo Ferme and Joao Leite (eds), Proceedings of the 14th European Conference on Logics in Artificial Intelligence, JELIA 2014. Lecture Notes in Artificial Intelligence 8761, pp. 543-557. Springer, 2014.
    DOI: doi.org/10.1007/978-3-319-11558-0_38
  • Muhammad Taimoor Khan, Wolfgang Schreiner. Towards the Formal Specification and Verification of Maple Programs. In: Johan Jeuring et al (eds), Intelligent Computer Mathematics, CICM 2012. Lecture Notes in Artificial Intelligence 7362, pp. 231-247. Springer, 2012.
    DOI: doi.org/10.1007/978-3-642-31374-5\_16
  • Tudor Jebelean, Bruno Buchberger, Temur Kutsia, Nikolaj Popov, Wolfgang Schreiner, Wolfgang Windsteiger:
    Automated Reasoning. Hagenberg Research 2009: 63-101.
    DOI: doi.org/10.1007/978-3-642-02127-5\_3
  • Bruno Buchberger. Mathematical Theory Exploration. Invited talk at the Third International Joint Conference on Automated Reasoning, IJCAR 2006. Lecture Notes in Artificial Intelligence 4130, pp. 1-2. Springer, 2006.
  • Wolfgang Windsteiger, Bruno Buchberger, Markus Rosenkranz. Theorema. In: Freek Wiedijk (ed.), The Seventeen Provers of the World. Lecture Notes in Artificial Intelligence 3600, pp. 96-107. Springer, 2006.
    DOI: doi.org/10.1007/11542384\_14
  • Gabor Kusper. Solving the Resolution-Free SAT Problem by Hyper-Unit Propagation in Linear Time. Annals of Mathematics and Artificial Intelligence 43(1-4), pp. 129-136. 2005.
    DOI: doi.org/10.1007/s10472-005-0423-7
  • Bruno Buchberger, John A. Campbell (eds). Artificial Intelligence and Symbolic Computation, 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004, Proceedings. Lecture Notes in Artificial Intelligence 3249, Springer 2004.
  • Bruno Buchberger, Gaston Gonnet, Michiel Hazewinkel (eds). Mathematical Knowledge Management. Special Issue of Annals of Mathematics and Artificial Intelligence, 38(1-3), 2003.
  • Edward Blurock. Machine Learning. In: Walter G. Kropatsch and Horst Bischof (eds), Digital Image Analysis. Chapter 10. Springer, New York, 2001.
    DOI: doi.org/10.1007/0-387-21643-X_13
  • Witold Jacak, Bruno Buchberger, Sabine Stifter. Intelligent Systems Combining Reactive and Learning Capabilities. In: Robert Trappl (ed.), Proceedings of the 13th European Meeting on Cybernetics and Systems Research, pp. 77-82. Austrian Society for Cybernetic Studies, 1996.
  • Hoon Hong, Dongming Wang, Franz Winkler (eds). Algebraic Approaches to Geometric Reasoning. Special issue of Annals of Mathematics and Artificial Intelligence, 13(1-2), 1995.
  • Eugen E. Ardeleanu. Completion and invariant theory in symbolic computation and artificial intelligence. In: Jacques Calmet and John A. Campbell, (eds). Artificial Intelligence and Symbolic Mathematical Computing. AISMC 1992. Lecture Notes in Computer Science, vol 737, pp. 178-187. Springer, Berlin, Heidelberg, 1992.
    DOI: doi.org/10.1007/3-540-57322-4_12
  • Franz Winkler. Equational Theorem Proving and Rewrite Rule Systems. In: 5. Österreichische Artificial-Intelligence-Tagung, Johannes Retti and Karl Leidlmair (ed.), Informatik Fachberichte 208 (Subreihe Künstliche Intelligenz 2252), pp. 26-39. Springer-Verlag, 1989.
    DOI: doi.org/10.1007/978-3-642-74688-8_3
  • Bruno Buchberger. Automatisches Programmieren (Automated Programming). In: Artificial Intelligence — Eine Einfuehrung, Johannes Retti et al. (ed.), XLeitfäden der angewandten Informatik, vol. 2, pp. 175-203. Vieweg+Teubner Verlag, Wiesbaden, 1986.
    DOI: doi.org/10.1007/978-3-322-93997-5_9
  • Wolfgang Bibel, Bruno Buchberger. Towards a connection machine for logical inference. Future Generation Computer Systems 1(3), pp. 177-188, 1985.
    DOI: doi.org/10.1016/0167-739X(85)90019-6
  • Peter Hintenaus, Bruno Buchberger. The L-Language for the Parallel L-Machine (A Parallel Architecture for AI Applications). In: Harald Trost and Johannes Retti (eds), Österreichische Artificial Intelligence-Tagung. Informatik-Fachberichte, vol 106. Springer, Berlin, Heidelberg, 1985.
    DOI: doi.org/10.1007/978-3-322-93997-5_9
  • Bruno Buchberger. Survey on Automatic Programming. Invited talk at Spring School in Artificial Intelligence, Teisendorf, Germany, 1982.
  • Bruno Buchberger. Automatisches Beweisen und Künstliche Intelligenz (Automated Theorem Proving and Artificial Intelligence). Talk at the Institute of System Sciences, University of Linz, Austria. 1979