diff --git a/docs/mts/formal-notation.md b/docs/mts/formal-notation.md
index 2795fec..394457d 100644
--- a/docs/mts/formal-notation.md
+++ b/docs/mts/formal-notation.md
@@ -46,7 +46,7 @@
 
 ```ebnf
 File      = { Stmt } ;
-Stmt      = Expr , "." ;
+Stmt      = Expr , [ "," ] ;  (* comma separator is optional *)
 
 Expr      = DefExpr | EqExpr | NeqExpr | Term ;
 
@@ -100,9 +100,9 @@ Ctx       = "[" , AbitSeq , "]" ;
 У тебя явно зафиксированы: ориентированность, единственность, порождение равенства, guarded recursion.
 
 ```mts
-(s : F) != (F : s).
-(s : F) : (s = F).
-{ s : F, s : G } : (F = G).
+(s : F) != (F : s)
+(s : F) : (s = F)
+{ s : F, s : G } : (F = G)
 ```
 
 > Заметь: это ровно твой тезис “`:` и `=` — разные онтологические категории, но `:` порождает `=`”. 
@@ -112,20 +112,20 @@ Ctx       = "[" , AbitSeq , "]" ;
 Ты формулируешь её как “равенство сложных сводится к равенству компонентов” и даёшь схемы через `{…}`.
 
 ```mts
-((a -> b) = (c -> d)) : { a = c, b = d }.
-{ a = c, b = d } : ((a -> b) = (c -> d)).
+((a -> b) = (c -> d)) : { a = c, b = d }
+{ a = c, b = d } : ((a -> b) = (c -> d))
 
-(♂a = ♂b) : (a = b).
-(a = b) : (♂a = ♂b).
+(♂a = ♂b) : (a = b)
+(a = b) : (♂a = ♂b)
 
-(a♀ = b♀) : (a = b).
-(a = b) : (a♀ = b♀).
+(a♀ = b♀) : (a = b)
+(a = b) : (a♀ = b♀)
 
-(¬a = ¬b) : (a = b).
-(a = b) : (¬a = ¬b).
+(¬a = ¬b) : (a = b)
+(a = b) : (¬a = ¬b)
 
-(!a = !b) : (a = b).
-(a = b) : (!a = !b).
+(!a = !b) : (a = b)
+(a = b) : (!a = !b)
 ```
 
 ### 3.3 Кванторы форм: `∞`, `♂`, `♀`, `->`
@@ -134,20 +134,20 @@ Ctx       = "[" , AbitSeq , "]" ;
 “Фундаментальная теорема” про `r -> v : (r -> v)` тоже есть. 
 
 ```mts
-∞ : (∞ -> ∞).
+∞ : (∞ -> ∞)
 
-♂x : (♂x -> x).
-x♀ : (x -> x♀).
+♂x : (♂x -> x)
+x♀ : (x -> x♀)
 
-(r -> v) : (r -> v).
+(r -> v) : (r -> v)
 ```
 
 А “уникальность” акорня ты формулируешь как эквивалентность `x = (x -> x)` и `x = ∞`.
 Без введения отдельного `⇔` даём как две направленные аксиомы через `:`:
 
 ```mts
-(x = (x -> x)) : (x = ∞).
-(x = ∞) : (x = (x -> x)).
+(x = (x -> x)) : (x = ∞)
+(x = ∞) : (x = (x -> x))
 ```
 
 ### 3.4 Инверсия направления `¬` (замена твоего `-`)
@@ -157,14 +157,14 @@ x♀ : (x -> x♀).
 Чтобы не повторить внутреннюю несогласованность “и просто переворот, и совместимость”, фиксирую **одну когерентную схему**: инверсия переворачивает связь и рекурсивно применяется к компонентам (контравариантно):
 
 ```mts
-¬(a -> b) : (¬b -> ¬a).
-¬(a !-> b) : (¬b !-> ¬a).
+¬(a -> b) : (¬b -> ¬a)
+¬(a !-> b) : (¬b !-> ¬a)
 
-¬(♂x) : (x♀).
-¬(x♀) : (♂x).
-¬∞ : ∞.
+¬(♂x) : (x♀)
+¬(x♀) : (♂x)
+¬∞ : ∞
 
-¬¬x = x.
+¬¬x = x
 ```
 
 ### 3.5 Несвязь `!->` и смысловая дуальность `!`, `0/1`
@@ -175,23 +175,23 @@ x♀ : (x -> x♀).
 Делаем `!->` определением “негации связи”:
 
 ```mts
-!(a -> b) : (a !-> b).
-!(a !-> b) : (a -> b).
+!(a -> b) : (a !-> b)
+!(a !-> b) : (a -> b)
 
-!!x = x.
+!!x = x
 ```
 
 Определяем `1` как “единицу смысла” (у тебя это `♂∞ -> ∞♀`).
 
 ```mts
-1 : (♂∞ -> ∞♀).
+1 : (♂∞ -> ∞♀)
 ```
 
 А `0` задаём как дуал `1` через `!` (и тем самым выполняем твои пункты 4–5):
 
 ```mts
-!1 : 0.
-!0 : 1.
+!1 : 0
+!0 : 1
 ```
 
 (Отсюда, через “(s:F) : (s = F)” + симметрию равенства в ядре прувера, получатся привычные записи `0 = !1`, `1 = !0`.)
@@ -203,8 +203,8 @@ x♀ : (x -> x♀).
 Фиксируем новую пару:
 
 ```mts
-[ : (♂∞ -> ∞).
-] : (∞ -> ∞♀).
+[ : (♂∞ -> ∞)
+] : (∞ -> ∞♀)
 ```
 
 ### 3.7 Акс. левоассоциативности цепочек
@@ -212,8 +212,8 @@ x♀ : (x -> x♀).
 У тебя это отдельный “онтологический принцип группировки”.
 
 ```mts
-(a -> b -> c) = ((a -> b) -> c).
-(a -> (b -> c)) != ((a -> b) -> c).
+(a -> b -> c) = ((a -> b) -> c)
+(a -> (b -> c)) != ((a -> b) -> c)
 ```
 
 ---
diff --git a/docs/mts/specification-v0.1.md b/docs/mts/specification-v0.1.md
index f70d3c8..eab652c 100644
--- a/docs/mts/specification-v0.1.md
+++ b/docs/mts/specification-v0.1.md
@@ -67,7 +67,7 @@ EBNF:
 
 File      ::= { Stmt } ;
 
-Stmt      ::= Expr "." ;
+Stmt      ::= Expr [ "," ] ;  // comma separator is optional
 
 Expr      ::= DefExpr
             | EqExpr
diff --git a/examples/basic.mtl b/examples/basic.mtl
index 3cd4ac6..dbd756d 100644
--- a/examples/basic.mtl
+++ b/examples/basic.mtl
@@ -8,10 +8,10 @@
 // ========================================
 
 // Тождественность акорня самому себе
-∞ = ∞.
+∞ = ∞
 
 // Акорень равен связи с самим собой
-∞ = ∞ -> ∞.
+∞ = ∞ -> ∞
 
 // ========================================
 // А5. Самозамыкание начала
@@ -19,10 +19,10 @@
 // ========================================
 
 // Мужской оператор определяет самозамыкание начала
-♂v = ♂v -> v.
+♂v = ♂v -> v
 
 // Вложенность мужского оператора
-♂♂v = ♂♂v -> ♂v.
+♂♂v = ♂♂v -> ♂v
 
 // ========================================
 // А6. Самозамыкание конца
@@ -30,10 +30,10 @@
 // ========================================
 
 // Женский оператор определяет самозамыкание конца
-r♀ = r -> r♀.
+r♀ = r -> r♀
 
 // Вложенность женского оператора
-r♀♀ = r♀ -> r♀♀.
+r♀♀ = r♀ -> r♀♀
 
 // ========================================
 // А7. Аксиома инверсии
@@ -42,14 +42,14 @@ r♀♀ = r♀ -> r♀♀.
 // ========================================
 
 // Инверсия мужского оператора
-!♂x = x♀.
+!♂x = x♀
 
 // Инверсия женского оператора
-!x♀ = ♂x.
+!x♀ = ♂x
 
 // Инверсия акорня
-!♂∞ = ∞♀.
-!∞♀ = ♂∞.
+!♂∞ = ∞♀
+!∞♀ = ♂∞
 
 // ========================================
 // А11. Левоассоциативность связи
@@ -57,10 +57,10 @@ r♀♀ = r♀ -> r♀♀.
 // ========================================
 
 // Цепочка связей левоассоциативна
-a -> b -> c = (a -> b) -> c.
+a -> b -> c = (a -> b) -> c
 
 // Более длинная цепочка
-a -> b -> c -> d = ((a -> b) -> c) -> d.
+a -> b -> c -> d = ((a -> b) -> c) -> d
 
 // ========================================
 // Степенной оператор
@@ -68,31 +68,31 @@ a -> b -> c -> d = ((a -> b) -> c) -> d.
 // ========================================
 
 // a^2 = (a -> a)
-a^2 = a -> a.
+a^2 = a -> a
 
 // a^3 = ((a -> a) -> a)
-a^3 = (a -> a) -> a.
+a^3 = (a -> a) -> a
 
 // a^4 = (((a -> a) -> a) -> a)
-a^4 = ((a -> a) -> a) -> a.
+a^4 = ((a -> a) -> a) -> a
 
 // ========================================
 // Комбинированные выражения
 // ========================================
 
 // Применение ♂ к ∞
-♂∞ = ♂∞ -> ∞.
+♂∞ = ♂∞ -> ∞
 
 // Применение ♀ к ∞
-∞♀ = ∞ -> ∞♀.
+∞♀ = ∞ -> ∞♀
 
 // Комбинация ♂ и ♀
-♂∞♀ = (♂∞)♀.
+♂∞♀ = (♂∞)♀
 
 // ========================================
 // Неравенства
 // ========================================
 
 // Различные выражения не равны
-♂∞♀ != ∞.
-♂∞ != ∞♀.
+♂∞♀ != ∞
+♂∞ != ∞♀
diff --git a/examples/test-issue-48-error.mtl b/examples/test-issue-48-error.mtl
index af3405e..36d81e3 100644
--- a/examples/test-issue-48-error.mtl
+++ b/examples/test-issue-48-error.mtl
@@ -2,21 +2,21 @@
 // Примеры аксиом и формул
 
 // А4. Смысл (акорень): ∞ : (∞ -> ∞)
-∞ = ∞ -> ∞.
+∞ = ∞ -> ∞
 
 // А5. Самозамыкание начала: ♂x : (♂x -> x)
-♂v = ♂v -> v.
+♂v = ♂v -> v
 
 // А6. Самозамыкание конца: x♀ : (x -> x♀)
-r♀ = r -> r♀.
+r♀ = r -> r♀
 
 // А7. Инверсия
-!♂x = x♀.
-!x♀ = ♂x.)   // тут некорректная закрывающая скобка
+!♂x = x♀
+!x♀ = ♂x)   // тут некорректная закрывающая скобка
 
 // А11. Левоассоциативность
-a -> b -> c = (a -> b) -> c.
+a -> b -> c = (a -> b) -> c
 
 // Степени
-a^2 = a -> a.
-a^3 = (a -> a) -> a.
+a^2 = a -> a
+a^3 = (a -> a) -> a
diff --git a/examples/test-issue-48.mtl b/examples/test-issue-48.mtl
index 6a238dc..685ade6 100644
--- a/examples/test-issue-48.mtl
+++ b/examples/test-issue-48.mtl
@@ -2,21 +2,21 @@
 // Пример из issue #48 с ошибкой парсинга
 
 // А4. Смысл (акорень): ∞ : (∞ -> ∞)
-∞ = ∞ -> ∞.
+∞ = ∞ -> ∞
 
 // А5. Самозамыкание начала: ♂x : (♂x -> x)
-♂v = ♂v -> v.
+♂v = ♂v -> v
 
 // А6. Самозамыкание конца: x♀ : (x -> x♀)
-r♀ = r -> r♀.
+r♀ = r -> r♀
 
 // А7. Инверсия
-!♂x = x♀.
-!x♀ = ♂x.)   // тут некорректная закрывающая скобка
+!♂x = x♀
+!x♀ = ♂x)   // тут некорректная закрывающая скобка
 
 // А11. Левоассоциативность
-a -> b -> c = (a -> b) -> c.
+a -> b -> c = (a -> b) -> c
 
 // Степени
-a^2 = a -> a.
-a^3 = (a -> a) -> a.
+a^2 = a -> a
+a^3 = (a -> a) -> a
diff --git a/experiments/test-error-location.ts b/experiments/test-error-location.ts
index 4f177a9..3b3f768 100644
--- a/experiments/test-error-location.ts
+++ b/experiments/test-error-location.ts
@@ -33,7 +33,12 @@ if (result.errorLocation) {
 
   console.log('\nError context:')
   console.log('Line', errorLine + 1, ':', lines[errorLine])
-  console.log('Error at column', errorCol, '-> character:', JSON.stringify(lines[errorLine][errorCol]))
+  console.log(
+    'Error at column',
+    errorCol,
+    '-> character:',
+    JSON.stringify(lines[errorLine][errorCol])
+  )
 
   // Show visual pointer
   const pointer = ' '.repeat(errorCol) + '^'
diff --git a/src/core/parser.ts b/src/core/parser.ts
index 5f7e212..e03b8df 100644
--- a/src/core/parser.ts
+++ b/src/core/parser.ts
@@ -4,7 +4,7 @@
  *
  * Grammar (simplified):
  * File      ::= { Stmt }
- * Stmt      ::= Expr "."
+ * Stmt      ::= Expr [ "," ]  // comma separator is optional
  * Expr      ::= DefExpr | EqExpr | NeqExpr | Term
  * DefExpr   ::= Term ":" Term
  * EqExpr    ::= Term "=" Term
@@ -164,15 +164,29 @@ export class Parser {
     }
   }
 
-  /** Parse statement: Expr "." */
+  /** Parse statement: Expr ["," | newline]
+   * Commas and newlines are optional separators between statements.
+   * They are consumed if present but not required.
+   * Periods (.) are NOT supported as separators.
+   */
   private parseStatement(): Statement {
     const expr = this.parseExpr()
-    const dot = this.expect('DOT')
+
+    // Optional separator: consume comma if present
+    // Newlines are already consumed by whitespace skipping in lexer
+    if (this.check('COMMA')) {
+      const separator = this.advance()
+      return {
+        type: 'Statement',
+        expr,
+        loc: this.mergeLoc(expr.loc!, separator.loc),
+      }
+    }
 
     return {
       type: 'Statement',
       expr,
-      loc: this.mergeLoc(expr.loc!, dot.loc),
+      loc: expr.loc!,
     }
   }
 
@@ -430,9 +444,9 @@ export function parseWithRecovery(input: string): ParseResult {
   return parser.parseFileWithRecovery()
 }
 
-/** Parse single expression (without trailing dot) */
+/** Parse single expression */
 export function parseExpr(input: string): ASTNode {
-  const lexer = new Lexer(input + '.')
+  const lexer = new Lexer(input)
   const tokens = lexer.tokenize()
   const parser = new Parser(tokens)
   const file = parser.parseFile()
diff --git a/tests/e2e/editor.spec.ts b/tests/e2e/editor.spec.ts
index 8b525a1..2bacd9f 100644
--- a/tests/e2e/editor.spec.ts
+++ b/tests/e2e/editor.spec.ts
@@ -44,7 +44,7 @@ test.describe('aprover Web Interface', () => {
     const editor = page.locator('.code-input')
 
     // Clear editor and enter a simple valid formula
-    await editor.fill('∞ = ∞.')
+    await editor.fill('∞ = ∞')
 
     // Wait for results to update
     await expect(page.locator('.result-item')).toHaveCount(1)
@@ -53,7 +53,7 @@ test.describe('aprover Web Interface', () => {
 
   test('should show success indicator for valid equality', async ({ page }) => {
     const editor = page.locator('.code-input')
-    await editor.fill('a = a.')
+    await editor.fill('a = a')
 
     const resultItem = page.locator('.result-item')
     await expect(resultItem).toHaveClass(/success/)
@@ -64,7 +64,7 @@ test.describe('aprover Web Interface', () => {
     const editor = page.locator('.code-input')
     // Using different structures that cannot be unified:
     // ♂∞ (male of infinity) cannot equal ∞♀ (female of infinity)
-    await editor.fill('♂∞ = ∞♀.')
+    await editor.fill('♂∞ = ∞♀')
 
     const resultItem = page.locator('.result-item')
     await expect(resultItem).toHaveClass(/failure/)
@@ -80,7 +80,7 @@ test.describe('aprover Web Interface', () => {
 
   test('should verify infinity axiom (А4)', async ({ page }) => {
     const editor = page.locator('.code-input')
-    await editor.fill('∞ = ∞ -> ∞.')
+    await editor.fill('∞ = ∞ -> ∞')
 
     await expect(page.locator('.result-item.success')).toBeVisible()
     await expect(page.locator('.result-status')).toHaveText('✓')
@@ -88,28 +88,28 @@ test.describe('aprover Web Interface', () => {
 
   test('should verify male self-closing axiom (А5)', async ({ page }) => {
     const editor = page.locator('.code-input')
-    await editor.fill('♂v = ♂v -> v.')
+    await editor.fill('♂v = ♂v -> v')
 
     await expect(page.locator('.result-item.success')).toBeVisible()
   })
 
   test('should verify female self-closing axiom (А6)', async ({ page }) => {
     const editor = page.locator('.code-input')
-    await editor.fill('r♀ = r -> r♀.')
+    await editor.fill('r♀ = r -> r♀')
 
     await expect(page.locator('.result-item.success')).toBeVisible()
   })
 
   test('should verify inversion axiom (А7)', async ({ page }) => {
     const editor = page.locator('.code-input')
-    await editor.fill('!♂x = x♀.')
+    await editor.fill('!♂x = x♀')
 
     await expect(page.locator('.result-item.success')).toBeVisible()
   })
 
   test('should verify power expansion', async ({ page }) => {
     const editor = page.locator('.code-input')
-    await editor.fill('a^2 = a -> a.')
+    await editor.fill('a^2 = a -> a')
 
     await expect(page.locator('.result-item.success')).toBeVisible()
   })
@@ -117,9 +117,9 @@ test.describe('aprover Web Interface', () => {
   test('should verify multiple formulas', async ({ page }) => {
     const editor = page.locator('.code-input')
     await editor.fill(`
-∞ = ∞ -> ∞.
-♂v = ♂v -> v.
-r♀ = r -> r♀.
+∞ = ∞ -> ∞
+♂v = ♂v -> v
+r♀ = r -> r♀
 `)
 
     const results = page.locator('.result-item')
@@ -132,14 +132,14 @@ r♀ = r -> r♀.
 
   test('should verify inequality', async ({ page }) => {
     const editor = page.locator('.code-input')
-    await editor.fill('♂∞ != ∞♀.')
+    await editor.fill('♂∞ != ∞♀')
 
     await expect(page.locator('.result-item.success')).toBeVisible()
   })
 
   test('should handle left associativity (А11)', async ({ page }) => {
     const editor = page.locator('.code-input')
-    await editor.fill('a -> b -> c = (a -> b) -> c.')
+    await editor.fill('a -> b -> c = (a -> b) -> c')
 
     await expect(page.locator('.result-item.success')).toBeVisible()
   })
@@ -182,7 +182,7 @@ r♀ = r -> r♀.
   test('should collapse all AST nodes', async ({ page }) => {
     // Enter a formula to generate AST
     const editor = page.locator('.code-input')
-    await editor.fill('a -> b.')
+    await editor.fill('a -> b')
 
     // Wait for AST to render
     await expect(page.locator('.tree-root')).toBeVisible()
@@ -203,7 +203,7 @@ r♀ = r -> r♀.
   test('should expand all AST nodes after collapse', async ({ page }) => {
     // Enter a formula to generate AST
     const editor = page.locator('.code-input')
-    await editor.fill('a -> b.')
+    await editor.fill('a -> b')
 
     // Wait for AST to render
     await expect(page.locator('.tree-root')).toBeVisible()
@@ -222,7 +222,7 @@ r♀ = r -> r♀.
   test('should display node location in AST tree', async ({ page }) => {
     // Enter a simple formula
     const editor = page.locator('.code-input')
-    await editor.fill('a = a.')
+    await editor.fill('a = a')
 
     // Wait for AST to render
     await expect(page.locator('.tree-root')).toBeVisible()
@@ -235,7 +235,7 @@ r♀ = r -> r♀.
   test('should highlight source code when hovering AST node', async ({ page }) => {
     // Enter a simple formula
     const editor = page.locator('.code-input')
-    await editor.fill('a = a.')
+    await editor.fill('a = a')
 
     // Wait for AST to render
     await expect(page.locator('.tree-root')).toBeVisible()
@@ -254,7 +254,7 @@ r♀ = r -> r♀.
   test('should remove highlight when mouse leaves AST node', async ({ page }) => {
     // Enter a simple formula
     const editor = page.locator('.code-input')
-    await editor.fill('a = a.')
+    await editor.fill('a = a')
 
     // Wait for AST to render
     await expect(page.locator('.tree-root')).toBeVisible()
@@ -277,7 +277,7 @@ r♀ = r -> r♀.
   test('should toggle individual AST nodes', async ({ page }) => {
     // Enter a formula with nested structure
     const editor = page.locator('.code-input')
-    await editor.fill('a -> b.')
+    await editor.fill('a -> b')
 
     // Wait for AST to render with children visible
     await expect(page.locator('.tree-root')).toBeVisible()
@@ -413,7 +413,7 @@ r♀ = r -> r♀.
 
     test('should enable export buttons when results exist', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('a = a.')
+      await editor.fill('a = a')
 
       // Wait for verification to complete
       await expect(page.locator('.result-item')).toBeVisible()
@@ -493,7 +493,7 @@ r♀ = r -> r♀.
   test.describe('Enhanced Prover Features', () => {
     test('should display applied axioms badges', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('∞ = ∞ -> ∞.')
+      await editor.fill('∞ = ∞ -> ∞')
 
       // Wait for results
       await expect(page.locator('.result-item.success')).toBeVisible()
@@ -505,7 +505,7 @@ r♀ = r -> r♀.
 
     test('should show axiom badges with correct labels', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('∞ = ∞ -> ∞.')
+      await editor.fill('∞ = ∞ -> ∞')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -516,7 +516,7 @@ r♀ = r -> r♀.
 
     test('should show expand toggle for results with details', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('♂v = ♂v -> v.')
+      await editor.fill('♂v = ♂v -> v')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -526,7 +526,7 @@ r♀ = r -> r♀.
 
     test('should expand proof steps on click', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('∞ = ∞ -> ∞.')
+      await editor.fill('∞ = ∞ -> ∞')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -540,7 +540,7 @@ r♀ = r -> r♀.
 
     test('should display proof step index numbers', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('a = a.')
+      await editor.fill('a = a')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -554,7 +554,7 @@ r♀ = r -> r♀.
 
     test('should display proof step actions', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('a = a.')
+      await editor.fill('a = a')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -567,7 +567,7 @@ r♀ = r -> r♀.
 
     test('should collapse proof steps on second click', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('a = a.')
+      await editor.fill('a = a')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -583,7 +583,7 @@ r♀ = r -> r♀.
     test('should display hints for failed verification', async ({ page }) => {
       const editor = page.locator('.code-input')
       // This should fail: male and female are dual but not equal
-      await editor.fill('♂∞ = ∞♀.')
+      await editor.fill('♂∞ = ∞♀')
 
       await expect(page.locator('.result-item.failure')).toBeVisible()
 
@@ -594,7 +594,7 @@ r♀ = r -> r♀.
 
     test('should display hint icons', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('♂∞ = ∞♀.')
+      await editor.fill('♂∞ = ∞♀')
 
       await expect(page.locator('.result-item.failure')).toBeVisible()
 
@@ -604,7 +604,7 @@ r♀ = r -> r♀.
 
     test('should display related axiom in hints when applicable', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('♂∞ = ∞♀.')
+      await editor.fill('♂∞ = ∞♀')
 
       await expect(page.locator('.result-item.failure')).toBeVisible()
 
@@ -615,7 +615,7 @@ r♀ = r -> r♀.
 
     test('should show A5 axiom for male self-closing', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('♂v = ♂v -> v.')
+      await editor.fill('♂v = ♂v -> v')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -625,7 +625,7 @@ r♀ = r -> r♀.
 
     test('should show A6 axiom for female self-closing', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('r♀ = r -> r♀.')
+      await editor.fill('r♀ = r -> r♀')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -635,7 +635,7 @@ r♀ = r -> r♀.
 
     test('should show A1 axiom for structural equality', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('a = a.')
+      await editor.fill('a = a')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -645,7 +645,7 @@ r♀ = r -> r♀.
 
     test('should show axiom tooltip on hover', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('∞ = ∞ -> ∞.')
+      await editor.fill('∞ = ∞ -> ∞')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
@@ -658,7 +658,7 @@ r♀ = r -> r♀.
 
     test('should display axioms label', async ({ page }) => {
       const editor = page.locator('.code-input')
-      await editor.fill('a = a.')
+      await editor.fill('a = a')
 
       await expect(page.locator('.result-item.success')).toBeVisible()
 
diff --git a/tests/integration/mtl_formulas.test.ts b/tests/integration/mtl_formulas.test.ts
index e8130c3..e259342 100644
--- a/tests/integration/mtl_formulas.test.ts
+++ b/tests/integration/mtl_formulas.test.ts
@@ -21,7 +21,7 @@ import { createProverState, verify } from '../../src/core/prover'
  * Parse and verify a single formula string
  */
 function verifyFormula(formula: string): { success: boolean; message: string } {
-  const file = parse(formula + '.')
+  const file = parse(formula)
   const state = createProverState()
   const stmt = file.statements[0]
   const normalized = normalize(stmt.expr)
@@ -179,10 +179,10 @@ describe('Integration: mtl_formulas.mtc', () => {
 describe('Integration: Full pipeline test', () => {
   it('should process multiple statements', () => {
     const input = `
-      ∞ = ∞ -> ∞.
-      ♂v = ♂v -> v.
-      r♀ = r -> r♀.
-      !♂x = x♀.
+      ∞ = ∞ -> ∞
+      ♂v = ♂v -> v
+      r♀ = r -> r♀
+      !♂x = x♀
     `
     const file = parse(input)
     expect(file.statements).toHaveLength(4)
@@ -197,7 +197,7 @@ describe('Integration: Full pipeline test', () => {
 
   it('should normalize and verify power expressions correctly', () => {
     // Power expansion should work with normalizer
-    const input = 'a^5.'
+    const input = 'a^5'
     const file = parse(input)
     const stmt = file.statements[0]
     const normalized = normalize(stmt.expr)
diff --git a/tests/unit/parser.test.ts b/tests/unit/parser.test.ts
index 67e2e0a..8581eab 100644
--- a/tests/unit/parser.test.ts
+++ b/tests/unit/parser.test.ts
@@ -180,12 +180,30 @@ describe('Parser', () => {
   })
 
   describe('File parsing', () => {
-    it('should parse multiple statements', () => {
-      const file = parse('a = b. c = d.')
+    it('should parse multiple statements with commas', () => {
+      const file = parse('a = b, c = d')
       expect(file.type).toBe('File')
       expect(file.statements.length).toBe(2)
     })
 
+    it('should parse multiple statements with newlines', () => {
+      const file = parse('a = b\nc = d')
+      expect(file.type).toBe('File')
+      expect(file.statements.length).toBe(2)
+    })
+
+    it('should parse multiple statements without separators', () => {
+      const file = parse('a = b\nc = d\ne = f')
+      expect(file.type).toBe('File')
+      expect(file.statements.length).toBe(3)
+    })
+
+    it('should parse mixed separators (commas and newlines)', () => {
+      const file = parse('a = b\nc = d,\ne = f')
+      expect(file.type).toBe('File')
+      expect(file.statements.length).toBe(3)
+    })
+
     it('should parse empty file', () => {
       const file = parse('')
       expect(file.statements.length).toBe(0)
@@ -193,10 +211,6 @@ describe('Parser', () => {
   })
 
   describe('Error handling', () => {
-    it('should throw on missing dot', () => {
-      expect(() => parse('a = b')).toThrow(ParseError)
-    })
-
     it('should throw on unexpected token', () => {
       expect(() => parseExpr(')')).toThrow(ParseError)
     })
@@ -205,16 +219,16 @@ describe('Parser', () => {
   describe('Partial parsing with error recovery', () => {
     it('should return partial AST when error occurs after valid statements', () => {
       const input = `
-a = b.
-c = d.
+a = b
+c = d
 e = f)
       `.trim()
 
       const result = parseWithRecovery(input)
 
-      // Should have parsed first two statements successfully
+      // Should have parsed three statements successfully (e = f is valid)
       expect(result.file).not.toBeNull()
-      expect(result.file?.statements.length).toBe(2)
+      expect(result.file?.statements.length).toBe(3)
 
       // Should have error information
       expect(result.error).not.toBeNull()
@@ -225,7 +239,7 @@ e = f)
     it('should return null file when error occurs on first statement', () => {
       const input = `
 )
-a = b.
+a = b
       `.trim()
 
       const result = parseWithRecovery(input)
@@ -240,22 +254,22 @@ a = b.
 
     it('should handle error from issue #48 example', () => {
       const input = `
-∞ = ∞ -> ∞.
-♂v = ♂v -> v.
-r♀ = r -> r♀.
-!♂x = x♀.
-!x♀ = ♂x.)
-a -> b -> c = (a -> b) -> c.
+∞ = ∞ -> ∞
+♂v = ♂v -> v
+r♀ = r -> r♀
+!♂x = x♀
+!x♀ = ♂x)
+a -> b -> c = (a -> b) -> c
       `.trim()
 
       const result = parseWithRecovery(input)
 
-      // Line 5 is "!x♀ = ♂x.)" which parses as "!x♀ = ♂x." followed by stray ")"
+      // Line 5 is "!x♀ = ♂x)" which parses as "!x♀ = ♂x" followed by stray ")"
       // So 5 valid statements should be parsed (lines 1-5)
       expect(result.file).not.toBeNull()
       expect(result.file?.statements.length).toBe(5)
 
-      // Should have error on the closing paren after the dot
+      // Should have error on the closing paren
       expect(result.error).not.toBeNull()
       expect(result.error?.message).toContain('RPAREN')
       expect(result.errorLocation?.start.line).toBe(5)
@@ -263,8 +277,8 @@ a -> b -> c = (a -> b) -> c.
 
     it('should return no error when parsing is fully successful', () => {
       const input = `
-a = b.
-c = d.
+a = b
+c = d
       `.trim()
 
       const result = parseWithRecovery(input)
@@ -279,14 +293,14 @@ c = d.
     })
 
     it('should provide correct error location', () => {
-      const input = 'a = b.\nc = d).'
+      const input = 'a = b\nc = d)'
 
       const result = parseWithRecovery(input)
 
-      // Should have parsed first statement
-      expect(result.file?.statements.length).toBe(1)
+      // Should have parsed two statements (a = b and c = d are valid)
+      expect(result.file?.statements.length).toBe(2)
 
-      // Error should be on line 2
+      // Error should be on line 2 (the ')' part)
       expect(result.errorLocation?.start.line).toBe(2)
       expect(result.error?.message).toContain('RPAREN')
     })