New answers tagged lo.logic
0
Version 1.5 of Lisp (1955) supports homoiconicity. It's not a model of computation but it could still be interesting.
Sidenote: I wrote an implementation of Lisp 1.5 that supports homoiconicity.
9
A something that might be too long for a comment, based on the previous answer by Emil.
In the case you are interested in the complexity of such a logic, consider reading LICS'2015 paper by Joël Ouaknine, Antonia Lechner and Ben Worrell. A preprint is available here: https://www.cs.ox.ac.uk/people/james.worrell/LICS-main.pdf
According to the authors, the ...
21
($=$ is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as $\gcd$ has both a universal and an existential definition in terms of $|$, $+$, and $\le$:
$$\begin{align*}
\gcd(a,b)=c&\iff c\ge0\land c\mid a\land c\mid b\land\forall d\:(d\mid a\land d\mid b\to d\mid c)\\
&\iff c\ge0\land c\...
Top 50 recent answers are included
Related Tags
lo.logic × 482type-theory × 84
cc.complexity-theory × 70
reference-request × 65
pl.programming-languages × 58
lambda-calculus × 56
computability × 46
proof-theory × 26
descriptive-complexity × 24
sat × 22
proof-complexity × 20
automated-theorem-proving × 20
finite-model-theory × 20
model-checking × 19
automata-theory × 18
temporal-logic × 18
ct.category-theory × 17
dependent-type × 17
proof-assistants × 16
coq × 15
type-systems × 13
linear-logic × 13
ds.algorithms × 12
program-verification × 12
linear-temporal-logic × 12