# Towards Specifying Symbolic Computation

## TL;DR

This paper explores formal logic methods to specify symbolic computation algorithms that manipulate mathematical expressions, addressing the challenges of combining syntax and semantics.

## Contribution

It introduces a formal logic framework with undefinedness, quotation, and evaluation to specify syntax-based symbolic algorithms.

## Key findings

- Demonstrates specification of symbolic algorithms in formal logic
- Addresses the interplay of syntax and semantics in symbolic computation
- Provides a foundation for formal verification of symbolic algorithms

## Abstract

Many interesting and useful symbolic computation algorithms manipulate mathematical expressions in mathematically meaningful ways. Although these algorithms are commonplace in computer algebra systems, they can be surprisingly difficult to specify in a formal logic since they involve an interplay of syntax and semantics. In this paper we discuss several examples of syntax-based mathematical algorithms, and we show how to specify them in a formal logic with undefinedness, quotation, and evaluation.