Verantyx (avh-math) – Solvable Problems & Scope Guide
English
1. Purpose of This Guide
This guide explains what kinds of problems the current Verantyx database can and cannot handle. Verantyx is not a general-purpose AI; its reasoning ability is strictly bounded by its database and solvers. This limitation is intentional.
2. High-Level Scope of the Current DB
The current avh-math database is designed to handle problems that are:
- Symbolic (logical structures, not numeric-heavy)
- Rule-based (deterministic, not statistical)
- Explicitly stated (closed-world assumption)
- Verifiable by construction (reducible to formal logic)
3. Supported Problem Domains (Current)
3.1 Propositional Logic
The current DB and solvers fully support:
- Tautology checking
- Validity / invalidity of formulas
- Logical implication and contraposition
- Equivalence checking
- Explicit counterexample construction
Example Questions:
- "Is (A ∧ B) -> A valid?"
- "Does (A -> B) -> (~B -> ~A) hold for all valuations?"
3.2 Modal Logic (Kripke Semantics)
Support for basic modal logic includes:
- □ (Necessity) and ◇ (Possibility)
- Kripke frame semantics
- Frame conditions: Reflexive, Transitive, Symmetric (partial)
- Explicit counterexample models showing failing worlds and valuations.
Example Questions:
- "Is p -> □p valid in arbitrary Kripke frames?" (Returns DISPROVED with countermodel)
- "Is □p -> p valid in reflexive frames?" (Returns PROVED)
3.3 Axiom-Based Reasoning (Limited)
The DB includes foundational axioms for:
- Classical propositional logic
- Modal systems (K, T, S4, partial S5)
- This allows matching formulas against known schemas and highlighting missing assumptions.
4. What Verantyx Explicitly Does NOT Handle (Yet)
The current DB does not support:
- Continuous mathematics (Calculus, Real Analysis)
- Probability theory and Statistics
- Empirical reasoning or "Common Sense" inference
- Open-ended word problems requiring guessing or approximation.
If a problem requires statistical inference or implicit background knowledge, Verantyx will return UNKNOWN or NOT APPLICABLE. This is a safety feature.
5. Input Rules (Mandatory)
To ensure the system correctly identifies the logical target, you must follow these rules:
- Quote your formulas: Always enclose the logical part of your query in double quotes (
"..."). - Separation: This allows Verantyx to separate the instruction (natural language) from the problem (logic).
| Type | Example |
|---|---|
| ✅ Correct | Is "(A & B) -> A" always true? |
| ❌ Incorrect | Is (A & B) -> A always true? |
6. Best Query Patterns
The system works best when questions are clearly scoped and logically closed.
- Good: "In modal logic, under transitivity, is the following formula valid: '[]p -> [][]p'?"
- Bad: "Is this generally true?" or "Does this usually happen?"
6. How the DB Is Used During Reasoning
- Immediate matching: Checks against known axioms or known counterexamples.
- Constraint checking: Enforces domain restrictions and frame conditions.
- Boundary detection: Identifies where reasoning must stop and returns UNKNOWN instead of guessing.
7. Why This Limited Scope Is a Strength
- Hallucination is structurally impossible.
- Every answer is auditable and every failure is explicit.
- Verantyx prefers "I cannot prove this with the current database" over "This is probably true."
8. How This Scope Can Expand
Solvable problems expand by adding new DB entries or new solvers, not by retraining or scaling parameters. Evolution is transparent and domain-driven.
9. Summary
Verantyx is suitable for Formal Logic, Verification-oriented reasoning, and Safety-critical rule validation. It is not a general intelligence that guesses answers; it is a deterministic engine that proves them.
Japanese（日本語）
1. このガイドの目的
このガイドは、現在の Verantyx (avh-math) の DB で「何ができて、何ができないか」を明確に説明するためのものです。Verantyx は汎用 AI ではなく、その推論能力は DB とソルバーで厳密に制限されています。これは設計思想です。
2. 現在の DB の大枠の範囲
現在の avh-math DB が対応できる問題は、次をすべて満たすものです：
- 記号的である（論理構造、数値計算中心ではない）
- ルールベースである（決定論的、統計的ではない）
- 明示的に書かれている（閉じた世界の前提）
- 構造的に検証できる（形式論理に還元可能）
3. 対応している問題分野
3.1 命題論理
現在の DB とソルバーは以下を完全にサポートします：
- 恒真式判定
- 妥当性・非妥当性の判定
- 含意関係、対偶の評価
- 同値性チェック
- 明示的な反例（真理値割当）の生成
対応例：
- (A ∧ B) -> A は正しいか？
- (A -> B) -> (~B -> ~A) は常に成り立つか？
3.2 様相論理（Kripke 意味論）
以下の様相論理推論をサポートしています：
- □（必要性） および ◇（可能性）
- Kripke フレーム意味論
- 到達関係の条件：反射性、推移性、対称性（一部）
- 具体的反例モデルの構成（失敗した世界と真理値の表示）
対応例：
- _任意のフレームにおいて p -> □p は妥当か？_（反例を返します）
- _反射的なフレームにおいて □p -> p は妥当か？_（証明を返します）
3.3 公理ベース推論（限定的）
以下の基礎公理を DB に含んでいます：
- 古典命題論理の公理
- 様相論理体系（K, T, S4, S5 の一部）
- これにより、既知の公理スキーマとの照合や、不足している仮定の指摘が可能です。
4. 明確に「できない」こと
現在の DB では以下は扱いません：
- 連続的な数学（解析学、微分積分など）
- 確率論、統計学
- 経験則や「常識」に基づく推論
- 推測や近似を必要とするオープンエンドな文章題
統計的推論や暗黙の背景知識が必要な場合、Verantyx は UNKNOWN（不明）または NOT APPLICABLE（非該当）を返します。これは安全設計です。
5. 入力のルール（必須）
システムが論理的な対象を正確に識別するために、以下のルールを必ず守ってください。
- 式を引用符で囲む: クエリの論理式の部分は、必ずダブルクォーテーション（
"..."）で囲んでください。 - 役割の分離: これにより、Verantyx は指示（自然言語）と対象（論理）を明確に分離して処理できます。
| 形式 | 例 |
|---|---|
| ✅ 正しい例 | 「**(A & B) -> A**」は常に正しいか？ |
| ❌ 誤った例 | (A & B) -> A は常に正しいか？ |
6. 向いている質問の形
質問が明確に定義され、論理的に閉じている場合に最高の性能を発揮します。
- 良い例: 「様相論理において、推移性を仮定した場合、式 '[]p -> [][]p' は妥当か？」
- 悪い例: 「これは普通正しい？」「だいたいどうなる？」
6. DB の使われ方
- 既知ルールとの照合: 公理や既知の反例との即時マッチング。
- 制約・仮定チェック: ドメイン制限やフレーム条件の適用。
- 推論限界の検出: 推論が不可能な場所を特定し、推測せずに UNKNOWN を返します。
7. 制限が強みになる理由
- ハルシネーション（捏造）が構造的に不可能です。
- すべての回答が監査可能であり、失敗は明示されます。
- Verantyx は「おそらく正しい」と言うよりも、「現在のデータベースでは証明できません」と答えることを優先します。
8. 今後の拡張方法
対応できる問題の範囲は、DB エントリやソルバーの追加によってのみ拡張されます。再学習やパラメータの増大による拡張ではありません。 進化は透明で制御可能です。
9. まとめ
Verantyx は形式論理、検証重視の推論、安全性が最優先されるルール確認に適しています。答えを推測する汎用知能ではなく、数学的な厳密さで答えを証明・反証する決定論的エンジンです。