MASTERARBEIT / MASTER’S THESIS
Titel der Masterarbeit / Title of the Master‘s Thesis
On Hilbert’s Tenth Problem over
Rings of Algebraic Integers
verfasst von / submitted by
Tim Benedikt Herbstrith BSc
angestrebter akademischer Grad /
in partial fullment of the requirements for the degree of
Master of Science (MSc)
Wien, 2019 / Vienna 2019
Studienkennzahl lt. Studienblatt /
degree programme code as it appears
on the student record sheet:
UA 066 821
Studienrichtung lt. Studienblatt /
degree programme as it appears on
the student record sheet:
Masterstudium Mathematik
Betreut von / Supervisor: ao. Univ.-Prof. Mag. Dr. Christoph Baxa
https://github.com/tim6her/h10-over-rings-of-integers
Some Rights
Reserved
Contents
1 Prerequisites and central notions 1
2 Hilbert’s tenth problem 57
A Collected Haskell implementations 103
B Summaries 111
1 Prerequisites and central notions
1.1 Prerequisites from computability theory
2
1 3
≅
3
1
2
↕
𝑥 = 101
≠
𝑦 = 011
↕
1.1.1 Turing machines, problems, and decidability
01 01
01
0 1
1
101 011
§
_
§_01
start
halt
§ §
§
halt
halt
§
halt
0
0
overow
overow
0
return
1
return
1
overow
0
§
0 0 0 1
. . .
overflow
halt
start
§ _
§__
§001_0__
01
§
_
start
halt
delta
state
state’
delta "state" b = ("state'", b', m)
-- start by entering the "overflow" state ...
add1 "start" '§' = ("overflow", '§', 1 )
-- ... and stay in this state, as long as you read only '1'-s
add1 "overflow" '1' = ("overflow", '0', 1 )
-- if you read the first '0' or an empty cell replace it by '1'
-- and enter the "return" state to move the head to the first cell
add1 "overflow" '0' = ("return", '1', -1)
add1 "overflow" '_' = ("return", '1', -1)
-- we finish if we read '§' again or ...
add1 "return" '§' = ("halt", '§', 0 )
-- ... continue to move to the left and don't change the cell
-- content. Here `b` matches '0' or '1'
add1 "return" b = ("return", b , -1)
add1 _state _char = ("error", '_', 0 )
delta "state" 1 = ("state'", b', m )
delta "state" b = ("state''", b'', m')
state’
state
1
state”
state
1
1
add1
start
halt
overow
return
error
add1
error
add1
1101
1101
1 0
01
1
https://www.haskell.org/onlinereport/haskell2010
§
1 1 0 1
. . .
start
start
§
overow
§
§
1 1 0 1
. . .
overflow
overow
1
overow
0
§
0 1 0 1
. . .
overflow
overow
1
overow
0
§
0 0 0 1
. . .
overflow
overow
0
return
1
§
0 0 1 1
. . .
return
return
0
return
0
§
0 0 1 1
. . .
return
return
0
return
0
§
0 0 1 1
. . .
return
return
§
halt
§
§
0 0 1 1
. . .
halt
halt
§
halt
§
add1
1101
01
start
halt
accept
reject
start
1
1
1
reject
_
0
0
0
reject
_
_
accept
_
reject
_
_
accept
1
reject
0
accept
reject
start
halt
start
§
halt
§
start
halt
start
halt
start
halt
compose
start
compose
halt
halt
start
compose
11
-times
1
0
-- start by entering the "check" state and ...
tally "start" '§' = ("check", '§', 1 )
-- ... stay in this state while reading only '1'-s
tally "check" '1' = ("check", '1', 1 )
-- on reading '_' accept the input and clear the tape ...
tally "check" '_' = ("accept", '_', -1)
tally "accept" '1' = ("accept", '_', -1)
-- ...except for cell c(1), where you write a '1'
tally "accept" '§' = ("accept", '§', 1 )
tally "accept" '_' = ("halt", '1', -1)
-- however, if you read a '0' first, reject the input
-- by moving to the end of the input string ...
tally "check" '0' = ("rejectMR", '0', 1 )
tally "rejectMR" '_' = ("reject", '_', -1)
tally "rejectMR" b = ("rejectMR", b, 1 ) -- `b` matches '0' or '1'
-- ... and clear the tape except for cell c(1) where you
-- write a '0'
tally "reject" '§' = ("reject", '§', 1 )
tally "reject" '_' = ("halt", '0', -1)
tally "reject" b = ("reject", '_', -1) -- `b` matches '0' or '1'
tally _state _char = ("error", '_', 0 )
01
01
01
1
tally
start
halt
check
accept
reject
rejectMR
error
1
0
0
11
-times
0 11
-times
0 1
0
1
01
01
§
§
b
1
b
2
. . .
b
n−2
b
n−1
b
n
. . .
find non-empty
The machine nds the rst non-empty cell.
§
b
1
b
2
. . .
b
n−2
b
n−1
b
n
. . .
shift left b
n
The machine shifts the content of each cell one cell to the left …
§
b
1
b
2
b
3
. . .
b
n−1
b
n
. . .
shift left b
1
… until it reaches the end of tape symbol §.
§
b
1
b
2
b
3
. . .
b
n−1
b
n
. . .
find __
The machine nds two consecutive blank cells and starts over.
0
§
__
__
§
_
_
_
1 1
1 1
§
_
§
_
1 1
1
-- start by entering the "check" state
check1 "start" '§' = ("check", '§', 1 )
-- if you read a 1, check that the next cell is blank, and accept
check1 "check" '1' = ("check_blank", '1', 1 )
check1 "check_blank" '_' = ("accept", '_', -1)
-- if either of these conditions is not the case, reject
check1 "check" b = ("reject", b, 1 )
check1 "check_blank" b = ("reject", b, 1 )
-- accepting and rejecting actions
check1 "accept" 1 = ("halt", 1, -1)
check1 "reject" b = ("error", b, 1 )
check1 _state _char = ("error", '_', 0 )
10 01
1
1
10100
0
0
0
0
0
1 0
1
0
1
1
1 0
halt
1.1.2 Church-Turing thesis and the halting problem
2
3
1
0
2
3
4
1
4
1.2 Prerequisites from model theory
1.2.1 Formulae and models
1
e
1
e
01
01
1
e
1
e
1
e
0 0
0
1
0
1
x
1
x
2
x
3
x
1
x
1
x
2
x
2
1
x
1
x
1
x
2
x
2
1
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
i
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
x
1
x
n
0 1
x
i
1 1 1
-times
01 1 1
-times
a
a
m
1
m
k
m
i
5
5
6
x
1
x
2
x
3
x
2
x
1
x
2
1
x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
3
x
2
x
3
x
1
x
2
x
3
x
1
x
2
x
1
x
2
x
3
x
1
x
2
x
3
x
2
x
1
x
1
x
n
x
1
x
n
x
1
x
n
6
x
1
x
1
x
1
x
1
x
n
x
1
x
n
x
2
x
2
x
1
x
2
x
2
x
2
x
3
x
1
x
2
x
1
x
2
x
2
x
4
x
3
x
1
1.2.2 Morphisms, theories, and decidability
x
1
x
1
e x
1
x
1
e
x
1
x
1
x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
1
x
1
1
e
x
1
x
1
1
x
1
e
x
1
x
1
0x
2
x
1
x
2
1
Th
H10
x
i
1
x
i
k
x
i
1
x
i
k
Th
x
i
1
x
i
k
x
i
1
x
i
k
is atomic for , and
x
1
x
1
0x
2
x
1
x
2
1
Th
Th
x
1
x
2
1
1 0
H10
H10
1
2
4
3
x
1
x
2
x
3
Ex
1
x
2
Ex
2
x
3
Ex
3
x
1
x
1
x
2
x
3
Th
c
c
H10
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
is atomic for , and
there exists an atomic formula with
, or and
P
P
P
H10
c
x
i
1
x
i
d
P P
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
0
x
i
1
x
i
k
H10
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
x
x
j
x
-times
s
x
x
1
x
1
0
x
0 1
s
H10
∗
(𝔄)
Th
∃+
(𝔄)
Th(𝔄)
𝐷(𝔄)
H10(𝔄)
𝐷
∃+
(𝔄)
𝐷
𝑐
(𝔄)
Th
H10
x
i
1
x
i
k
x
i
1
x
i
k
Th
x
i
1
x
i
k
x
i
1
x
i
k
is atomic for
H10
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
x
i
1
x
i
k
is atomic for
there exists an atomic formula with
, or
ThH10
Th
H10
ThH10
Th
H10
0 1
H10
∗
(𝔒
𝐾
)
Th
∃+
(𝔒
𝐾
)
Th(𝔒
𝐾
)
𝐷(𝔒
𝐾
)
H10(𝔒
𝐾
)
𝐷
∃+
(𝔒
𝐾
)
𝐷
𝑐
(𝔒
𝐾
)
𝒦
Th
H10
H10
1.2.3 Computable structures and decidable models
ar
FC R
F
R
C
1
1
11011
0 1 1
0
0
c
n1
c
n
1
c
n
H10
x
1
x
n
x
1
x
n
H10
1.3 Prerequisites from number theory
1.3.1 Number elds and rings of algebraic integers
1.3.2 Ideals of
7
7
prime ideal
8
prime ideal
prime ideal
prime ideal
8
prime ideal
1.3.3 Geometry of numbers
𝐷
𝑒
1
𝑒
2
9
9
10
10
ႼႵᆡ
ႼႴᆡ ႼႳᆡ
ႼႲᆡ Ⴒᆡ
Ⴓᆡ Ⴔᆡ
Ⴕᆡ
ႼႴᆡ
ႼႳᆡ
ႼႲᆡ
Ⴒᆡ
Ⴓᆡ
Ⴔᆡ
Ⴑ
ᆂ
0
1
;
0 + ℤ = 1 + ℤ
1.3.4 Absolute values and local elds
2 Hilbert’s tenth problem
2.1 Dierent perspectives on an old problem
2.1.1 Diophantine equations and sets
1
2
3
1
0
0 1
1
2
3
1 0
α α
𝑥
2
+ 𝑦
2
= 1
−1 ≤ 𝑥 ≤ 1
x
1
x
n
y
1
y
m
y
1
y
m
y
1
y
m
H10
H10
H10
2.1.2 Purely Diophantine sets
x
1
x
n
y
1
y
m
y
1
y
m
y
1
y
m
H10
∗
(𝔒
𝐾
)
Th
∃+
(𝔒
𝐾
)
Th(𝔒
𝐾
)
𝐷(𝔒
𝐾
)
H10(𝔒
𝐾
)
𝐷
∃+
(𝔒
𝐾
)
𝐷
𝑐
(𝔒
𝐾
)
𝒦
H10
2.1.3 Related problems
Th
4
Th
H10
y
1
y
m
y
1
y
m
H10
H10
H10
4
2.2 Some structural results
H10
H10
H10
H10
101
-times
-times
2.3 Hilbert’s tenth problem over totally real number elds and
number elds with one pair of non-real embeddings
2.3.1 Finitely many easy lemmas
even
odd
even
odd
odd
-times
2.3.2 Diophantine denition of over
by (iv)
even
odd
Lem. 2.3.3.(ii)
even
odd
H10
H10
A Collected Haskell implementations
A.1 Simulating Turing machines
https://github.com/
tim6her/h10-turing-machines
git clone https://github.com/tim6her/h10-turing-machines.git
cd h10-turing-machines
cabal setup && cabal build && cabal install
ghci
>>> import Automaton.TuringMachine
>>> :l tally
>>> let d = toTransition tally "error" -- mark the errornous state
>>> let turing = TuringMachine "start" '_' "halt" d
>>> "§1111" >>> turing -- Tally encoding of 4
Just "§1"
>>> "§1011" >>> turing -- Not tally encoded
Just "§0"
A.2 Polynomials
{-# LANGUAGE RebindableSyntax #-}
module Monomial
( Monomial
, (<*>)
, idt
, mfromList
, clean
) where
import NumericPrelude
import Data.Map (Map, delete, empty, foldrWithKey, fromList, member, insert,
insertWith, (!))
import Algebra.Monoid as Monoid
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
-- | Monomials are mappings from ZZ to NN with finite support
newtype Monomial = Monomial (Map Integer Integer) deriving (Eq, Ord)
instance Monoid.C Monomial where
idt = Monomial empty
(<*>) = mmul
instance Show Monomial where
show (Monomial m)
| m == empty = "1"
| otherwise = foldrWithKey
(\x e sh -> "X" ++ show x ++ "^" ++ show e ++ " " ++ sh)
"" m
-- | Creates monomials from list of tuples
--
-- Left entry is index of indeterminate, right index is power of the
-- indeterminate
--
-- === Example
-- >>> mfromList [(1, 2), (0, 3), (4, 7)]
-- X0^3 X1^2 X4^7
mfromList :: [(Integer, Integer)] -> Monomial
mfromList l = clean $ Monomial $ fromList l
-- | Multiplies two monomials
--
-- === Example
-- >>> mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])
-- X1^2 X2^5 X3^2
mmul :: Monomial -> Monomial -> Monomial
mmul xx@(Monomial m1) yy@(Monomial m2)
| m1 == empty = yy
| m2 == empty = xx
| otherwise = clean $ Monomial $ foldrWithKey
(\x e m -> if x `member` m
then insertWith (+) x e m
else insert x e m)
m2 m1
clean :: Monomial -> Monomial
clean (Monomial m)
| m == empty = (Monomial m)
| otherwise = Monomial $ foldrWithKey
(\x e m -> if e <= 0
then delete x m
else m)
m m
-- * Testing
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Tests" [properties, unitTests]
properties :: TestTree
properties = testGroup "Properties" [qcProps]
qcProps = testGroup "Axioms of monoids"
[ QC.testProperty "left multiplication by identity" $
\x -> (let m = mfromList (x :: [(Integer, Integer)])
in idt <*> m == m)
, QC.testProperty "right multiplication by identity" $
\x -> (let m = mfromList (x :: [(Integer, Integer)])
in m <*> idt == m)
, QC.testProperty "associativity" $
\x y z -> (let m1 = mfromList (x :: [(Integer, Integer)])
m2 = mfromList (y :: [(Integer, Integer)])
m3 = mfromList (z :: [(Integer, Integer)])
in (m1 <*> m2) <*> m3 == m1 <*> (m2 <*> m3))
, QC.testProperty "commutativity" $
\x y -> (let m1 = mfromList (x :: [(Integer, Integer)])
m2 = mfromList (y :: [(Integer, Integer)])
in m1 <*> m2 == m2 <*> m1)
]
unitTests = testGroup "Unit tests"
[ testCase "show X0^3 X1^2 X4^7" $
show (mfromList [(1, 2), (0, 3), (4, 7)]) @?= "X0^3 X1^2 X4^7 "
, testCase "sample multiplication" $
show (mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])) @?=
"X1^2 X2^5 X3^2 "
, testCase "test clean" $
mfromList [(1, 0), (2, 0), (3, 1)] @?= mfromList [(3, 1)]
]
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
import NumericPrelude
import qualified Monomial
import qualified Data.Map as Map
import Algebra.Monoid as Monoid
import Algebra.Ring as Ring
import Algebra.Module as Module
import Algebra.Additive as Additive
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
-- | Polynomials over a ring R are finitely supported functions
-- from the set of monomials to R
newtype Polynomial a = Polynomial (Map.Map Monomial.Monomial a)
-- | Polynomials form an additive (abelian) group
instance (Ring.C a, Eq a) => Additive.C (Polynomial a) where
zero = Polynomial Map.empty
(+) = padd
negate (Polynomial m) = Polynomial $ Map.map negate m
-- | Polynomials from an R-module
instance (Ring.C a, Eq a) => Module.C a (Polynomial a) where
(*>) 0 _ = zero
(*>) a (Polynomial m) = Polynomial $ Map.map (a*) m
-- | Polynomials form a ring with unit
instance (Ring.C a, Eq a) => Ring.C (Polynomial a) where
one = pfromList [(1, [])]
(*) p@(Polynomial m1) q
| p == zero = zero
| q == zero = zero
| p == one = q
| q == one = p
| otherwise = Map.foldrWithKey
(\mono coeff poly -> (coeff *> mono `mmul` q) + poly)
0 m1
-- | Two polynomials are equal if their difference is zero
instance (Ring.C a, Eq a) => Eq (Polynomial a) where
(==) p q = let (Polynomial m) = p - q in m == Map.empty
instance (Show a, Eq a) => Show (Polynomial a) where
show (Polynomial p)
| p == Map.empty = "0"
| otherwise = Map.foldrWithKey
(\m a sh -> show a ++ " " ++ show m ++ "+ " ++ sh)
"" p
-- | Adds two polynomials over the same ring
--
-- If a coefficient of a monoid equals 0 the monoid is dropped out of the map
padd :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a -> Polynomial a
padd p@(Polynomial m1) q@(Polynomial m2)
| m1 == Map.empty = q
| m2 == Map.empty = p
| otherwise = clean $ Polynomial $ Map.foldrWithKey
(\mono coeff poly -> if mono `Map.member` poly
then Map.insertWith (+) mono coeff poly
else Map.insert mono coeff poly)
m2 m1
mmul :: (Ring.C a, Eq a) => Monomial.Monomial -> Polynomial a -> Polynomial a
mmul mono poly@(Polynomial mp)
| mono == Monomial.idt = Polynomial mp
| poly == zero = zero
| otherwise = Polynomial $ Map.mapKeys (mono Monomial.<*>) mp
-- | Generate polynomials from lists
pfromList :: (Ring.C a, Eq a) => [(a, [(Integer, Integer)])] -> Polynomial a
pfromList [] = zero
pfromList ((a, m):l) = deepClean . clean $ (Polynomial $ Map.singleton
(Monomial.mfromList m) a) + pfromList l
-- | Comfort function for creating polynomials
--
-- === Example
-- >>> 2 *> ((x 1 + x 2) * (x 1 - x 2)) == 2 *> x 1 ^ 2 - 2 *> x 2 ^ 2
-- True
x :: (Ring.C a, Eq a) => Integer -> Polynomial a
x i = pfromList [(1, [(i, 1)])]
-- | Remove monoids with coefficient zero from support
clean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a
clean (Polynomial m) = Polynomial $ Map.foldrWithKey
(\mono coeff poly -> if coeff == 0
then Map.delete mono poly
else poly)
m m
-- | Remove variables with power zero from monomials
--
-- This function runs in O(n log(n)) so use it sparsely
deepClean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a
deepClean (Polynomial m) = Polynomial $ Map.mapKeys Monomial.clean m
-- * Testing
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Tests" [properties, unitTests]
properties :: TestTree
properties = testGroup "Properties" [qcAddProps, qcModProps,
localOption (QuickCheckTests 5) qcRingProps,
qcAlgebraProps]
qcAddProps = testGroup "Group axioms for addition"
[ QC.testProperty "addition is commutative" $
\x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in p + q == q + p)
, QC.testProperty "addition is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 + p2) + p3 == p1 + (p2 + p3))
, QC.testProperty "addition by zero" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p + zero == p)
, QC.testProperty "addition with inverse" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p - p == zero)
]
qcModProps = testGroup "Module axioms"
[ QC.testProperty "first distributive law" $
\a x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p + q) == a *> q + a *> p)
, QC.testProperty "second distributive law" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a + b :: Int) *> p == a *> p + b *> p)
, QC.testProperty "multiplications commute" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a * b :: Int) *> p == a *> (b *> p))
, QC.testProperty "multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (one :: Int) *> p == p)
]
qcRingProps = testGroup "Ring axioms"
[ QC.testProperty "multiplication is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 * p2) * p3 == p1 * (p2 * p3))
, QC.testProperty "left multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in one * p == p)
, QC.testProperty "right multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p * one == p)
, QC.testProperty "distributive law" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in p1 * (p2 + p3) == p1 * p2 + p1 * p3)
]
qcAlgebraProps = testGroup "Algebra axioms"
[ QC.testProperty "multiplications commute" $
\x y a -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p1 * p2) == (a *> p1) * p2)
]
unitTests = testGroup "Unit tests"
[ testCase "sample polynomial" $
show (pfromList [(1, [(1, 2), (3, 4)]), (-4, [(1, 4), (2, 3)])]
:: Polynomial Int) @?= "1 X1^2 X3^4 + -4 X1^4 X2^3 + "
, testCase "test equality" $
pfromList [(0, [(1, 1)])] @?= (zero :: Polynomial Int)
]
B Summaries
B.1 Zusammenfassung
B.2 Summary
List of Figures
add1
1101
Bibliography
http://www.jstor.org/stable/2269326
10.2307/2371045
10.2307/2318447
http://www.jstor.org/stable/2318447
10.1016/j.amc.2005.09.066
https://doi.org/10.1016/j.amc.2005.09.066
10.2307/1998133
10.2307/2040720
10.1112/jlms/s2-18.3.385
10.1515/crll.1988.388.189 https://doi.org/10.1515/crll.1988.388.189
10.1112/jlms/s1-8.1.18
10.1007/BF01700692 https://doi.org/10.1007/BF01700692
10.1090/S0273-0979-00-00881-8
10.1007/978-3-642-75306-0
10.1215/S0012-7094-36-00227-2
https://doi.org/10.1215/S0012-7094-36-00227-2
10.1007/978-3-642-54936-6_5
10.1007/978-1-4613-0041-0
https://doi.org/10.1007/978-1-4613-0041-0
https://www.ebook.de/de/product/3665990/david_marker_model_theory_an_
introduction.html
www.jmilne.org/math/
http://www.logic.univie.ac.at/~muellem3/TCS.pdf
http://ubdata.univie.ac.at/AC05622932
10.4310/MRL.2013.v20.n5.a12
10.2307/2047021
https://doi.org/10.2307/2047021
http://www.ams.org/notices/200803/tx080300344p.pdf
10.1007/3-540-45455-1_4
10.1090/S0002-9904-1944-08111-1
https://doi.org/10.1090/S0002-9904-1944-08111-1
10.2307/2266510
10.2307/2033628
https://doi.org/10.2307/2033628
10.2307/2266685
10.2307/2269028
10.1515/crll.1986.368.127
https://doi.org/10.1515/crll.1986.368.127
10.1002/cpa.3160420805
https://doi.org/10.1002/cpa.3160420805
10.1002/cpa.3160420703
https://doi.org/10.1090/conm/270/04370
http://www.ebook.de/de/product/6433593/alexandra_shlapentokh_hilbert_s_
tenth_problem_diophantine_classes_and_extensions_to_global_fields.html
http://math.cornell.edu/~shore/papers/pdf/proc4t.pdf
10.1016/S0049-237X(99)80028-7
http://www.sciencedirect.com/science/article/pii/S0049237X99800287
http://eudml.org/doc/212515
10.1112/plms/s2-42.1.230
https://doi.org/10.1112/plms/s2-42.1.230
