summaryrefslogtreecommitdiffstats
path: root/content/zettel/3d2b1b.md
blob: 35cf0c9a90fea5dc5abffad9f5ef60f9328e24c9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
+++
title = "Atom Table"
date = "2022-08-08"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3d2b1a"]
forwardlinks = ["3d2b1c", "3d2b1d"]
zettelid = "3d2b1b"
+++

To be able to support various theories, atoms are used instead of
literals so that additional operations in different theories can be
represented. This allows for application of a function to arguments, for
example an `OZlt` operation, as well as simple variables or constants of
different types. The atoms can either contain these concrete operations
that are part of a theory directly, or they will refer to uninterpreted
functions that are declared in the operation table ([\#3d2b1c]).
Variables can be the same and will refer to variables declared in the
variable table ([\#3d2b1d]).

  [\#3d2b1c]: /zettel/3d2b1c
  [\#3d2b1d]: /zettel/3d2b1d