bill
b758d7ea60
- src/types.hpp: complete UCWM type system in C++20 — 19 enums, 11 facet data types, all core structs (CanonicalObject, Constraint, Facet, GateSignal, WorldState, etc.) with full JSON round-trip serialization - src/main.cpp: smoke test — constructs apple-problem WorldState by hand, serializes to JSON - tests/test_types.cpp: 19 tests, 123 assertions, all passing - CMakeLists.txt: CMake + CPM build with nlohmann/json, spdlog, Catch2 - schemas/: JSON Schema contracts for all UCWM data types - gates/, specialists/, resolver/, synthesis/: language-agnostic interface contracts and domain specs for all pipeline layers - docs/: architecture, vocabulary, decision matrices, roadmap (6 phases, 28 sprints), sprint_001, implementation_constraints Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
124 lines
3.4 KiB
Markdown
124 lines
3.4 KiB
Markdown
# Logic Specialist
|
|
|
|
**specialist_id:** `logic`
|
|
**trigger_gates:** `has_logical_negation`, `has_comparison`, `has_constraint`
|
|
|
|
---
|
|
|
|
## Responsibility
|
|
|
|
The logic specialist handles negation, implication, contradiction, quantifiers, and truth status. It attaches LogicalFacets to propositions and claims, and emits logical constraints that the resolver uses to detect contradictions and propagate truth values.
|
|
|
|
---
|
|
|
|
## Manifest
|
|
|
|
```
|
|
declared_facet_kinds:
|
|
- logical
|
|
|
|
declared_constraint_types:
|
|
- truth_value
|
|
- implies
|
|
- negates
|
|
- contradicts
|
|
- requires
|
|
- exclusive_or
|
|
- universally_quantified
|
|
- existentially_quantified
|
|
|
|
budget_caps:
|
|
max_objects_proposed: 4
|
|
max_facets_emitted: 8
|
|
max_constraints_emitted: 10
|
|
max_merges: 0
|
|
max_splits: 0
|
|
```
|
|
|
|
---
|
|
|
|
## Output: LogicalFacet
|
|
|
|
Attach to objects of kind `proposition`, `claim`, or `event` with a truth dimension.
|
|
|
|
```
|
|
LogicalFacet fields used:
|
|
- truth_status: "true" | "false" | "unknown" | "hypothetical" | "negated" | "asserted"
|
|
- quantifier: "universal" | "existential" | "none"
|
|
- implies_refs: [proposition_ids this implies]
|
|
- negates_refs: [proposition_ids this negates]
|
|
- contradicts_refs: [proposition_ids this contradicts]
|
|
```
|
|
|
|
---
|
|
|
|
## Output: Constraints
|
|
|
|
### `truth_value(P, status)`
|
|
|
|
Sets the explicit truth status of a proposition.
|
|
|
|
```
|
|
{
|
|
"constraint_type": "truth_value",
|
|
"argument_refs": ["P1"],
|
|
"polarity": "positive",
|
|
"strength": "hard",
|
|
"expression": "truth(P1) = false"
|
|
}
|
|
```
|
|
|
|
### `negates(P1, P2)`
|
|
|
|
P1 is the logical negation of P2. If P1 is true, P2 is false, and vice versa.
|
|
|
|
### `implies(P1, P2)`
|
|
|
|
If P1 is true, P2 must be true. Defeasible by default unless marked hard.
|
|
|
|
### `contradicts(P1, P2)`
|
|
|
|
P1 and P2 cannot both be true. Strength is always hard.
|
|
|
|
### `requires(A, B)`
|
|
|
|
A requires B to hold. Equivalent to `implies(A, B)` but semantically marks a dependency rather than a logical implication.
|
|
|
|
### `exclusive_or(P1, P2)`
|
|
|
|
Exactly one of P1 or P2 is true.
|
|
|
|
---
|
|
|
|
## Negation handling
|
|
|
|
Negation is the most error-prone logical operation. Rules:
|
|
|
|
1. Surface negation (e.g., `not`, `isn't`) does not always mean logical negation of a proposition — it may be just semantic modification.
|
|
2. When `has_logical_negation` fires, the logic specialist inspects whether the negation applies to:
|
|
- A predicate (`Alice is NOT happy` → LogicalFacet truth_status = negated)
|
|
- A quantifier (`NOT all → some are not`)
|
|
- A condition (`unless X` → implies(NOT X, consequence))
|
|
3. Emit `truth_value` constraints conservatively — only when confident the scope of negation is correctly identified.
|
|
|
|
---
|
|
|
|
## Contradiction detection support
|
|
|
|
The logic specialist does not resolve contradictions. It emits `contradicts` constraints when it detects that two propositions in WorldState logically oppose each other. The resolver handles contradiction resolution.
|
|
|
|
```
|
|
if P1 has truth_status = true AND P2 = negation_of(P1):
|
|
emit contradicts(P1, P2) with strength = hard
|
|
```
|
|
|
|
---
|
|
|
|
## Contract test requirements
|
|
|
|
- Given `Alice is not happy`, must emit a LogicalFacet on `P_alice_happy` with `truth_status: negated`
|
|
- Given `If it rains, the ground is wet`, must emit `implies(E_rain, S_ground_wet)`
|
|
- Must not emit temporal or quantity constraints
|
|
- Contradiction constraints must reference two objects that exist in WorldState
|
|
- All emitted constraints must have `source_module: logic`
|