From ca95f9d603a5551224fa486a141695cadd60370a Mon Sep 17 00:00:00 2001 From: Batixx Date: Thu, 26 Feb 2026 15:46:49 +0100 Subject: [PATCH 01/12] com --- packages/core/src/Formula.ts | 31 +++++++++---- packages/core/src/Logic/Derivations.ts | 15 ++++--- packages/core/src/Logic/Prover.ts | 45 ++++++++++++++----- packages/core/src/Logic/index.ts | 20 +++++---- packages/core/src/Trait.ts | 5 ++- packages/core/src/index.ts | 8 +++- .../src/components/Shared/Formula/Atom.svelte | 12 +++-- .../components/Traits/FilterButtons.svelte | 11 +++++ .../src/components/Traits/Related.svelte | 15 +++++-- .../viewer/src/components/Traits/Value.svelte | 6 ++- packages/viewer/src/models/Traits.ts | 3 ++ packages/viewer/src/stores/deduction.ts | 2 +- packages/viewer/src/types/index.ts | 8 ++-- 13 files changed, 134 insertions(+), 47 deletions(-) diff --git a/packages/core/src/Formula.ts b/packages/core/src/Formula.ts index dd9c3aec..29fb8a8c 100644 --- a/packages/core/src/Formula.ts +++ b/packages/core/src/Formula.ts @@ -3,8 +3,10 @@ import { parse as _parse } from './Formula/Grammar.js' import { union } from './Util.js' +export type TruthValue = boolean | 'undecidable' + type F

= - | { kind: 'atom'; property: P; value: boolean } + | { kind: 'atom'; property: P; value: TruthValue } | { kind: 'or'; subs: F

[] } | { kind: 'and'; subs: F

[] } @@ -12,7 +14,7 @@ function atomSchema

(p: z.ZodSchema

): z.ZodSchema> { return z.object({ kind: z.literal('atom'), property: p, - value: z.boolean(), + value: z.union([z.boolean(), z.literal('undecidable')]), }) as any } @@ -34,7 +36,7 @@ export const formulaSchema =

(p: z.ZodSchema

): z.ZodSchema> => export interface Atom { kind: 'atom' property: P - value: boolean | X + value: TruthValue | X } export interface And { @@ -59,7 +61,7 @@ export function or(...subs: Formula[]): Or { export function atom( property: P, - value: boolean | X = true, + value: TruthValue | X = true, ): Atom { return { kind: 'atom', property, value } } @@ -78,6 +80,7 @@ export function render(f: Formula, term: (t: T) => string): string { case 'atom': // eslint-disable-next-line no-case-declarations const name = term(f.property) + if (f.value === 'undecidable') return '⊬' + name return f.value ? name : '¬' + name case 'and': return '(' + f.subs.map(sf => render(sf, term)).join(' ∧ ') + ')' @@ -86,9 +89,21 @@ export function render(f: Formula, term: (t: T) => string): string { } } +export function hasUndecidable(f: Formula): boolean { + switch (f.kind) { + case 'atom': + return f.value === 'undecidable' + default: + return f.subs.some(hasUndecidable) + } +} + export function negate

(formula: Formula

): Formula

{ switch (formula.kind) { case 'atom': + if (formula.value === 'undecidable') { + throw new Error('Cannot negate an undecidable atom') + } return atom(formula.property, !formula.value) case 'and': return or(...formula.subs.map(negate)) @@ -130,7 +145,7 @@ export function compact( export function evaluate( f: Formula, - traits: Map, + traits: Map, ): boolean | undefined { let result: boolean | undefined @@ -192,8 +207,8 @@ type Serialized = | { and: Serialized[] } | { or: Serialized[] } | { inner: Serialized } - | { property: string; value: boolean | X } - | Record + | { property: string; value: TruthValue | X } + | Record export function fromJSON(json: Serialized): Formula { if ('and' in json && typeof json.and === 'object') { @@ -211,7 +226,7 @@ export function fromJSON(json: Serialized): Formula { throw `cannot cast object with ${entries.length} keys to atom` } - if (typeof entries[0][1] !== 'boolean') { + if (typeof entries[0][1] !== 'boolean' && entries[0][1] !== 'undecidable') { throw `cannot cast object with non-boolean value` } diff --git a/packages/core/src/Logic/Derivations.ts b/packages/core/src/Logic/Derivations.ts index ef072910..893802c6 100644 --- a/packages/core/src/Logic/Derivations.ts +++ b/packages/core/src/Logic/Derivations.ts @@ -1,10 +1,11 @@ +import { type TruthValue } from '../Formula.js' import { Id } from './Types.js' type Evidence = [TheoremId, PropertyId[]] export type Derivation = { property: PropertyId - value: boolean + value: TruthValue proof: Proof } @@ -16,17 +17,17 @@ export type Proof = { export class Derivations { private evidence: Map> private given: Set - private traits: Map + private traits: Map constructor(assumptions: PropertyId[] = []) { this.given = new Set(assumptions) this.evidence = new Map>() - this.traits = new Map() + this.traits = new Map() } addEvidence( property: PropertyId, - value: boolean, + value: TruthValue, theorem: TheoremId, support: PropertyId[], ): void { @@ -34,10 +35,14 @@ export class Derivations { this.traits.set(property, value) } + overrideGiven(property: PropertyId): void { + this.given.delete(property) + } + all(): Derivation[] { const result: Derivation[] = [] - this.traits.forEach((value: boolean, property: PropertyId) => { + this.traits.forEach((value: TruthValue, property: PropertyId) => { const proof = this.proof(property) if (!proof || proof === 'given') { return diff --git a/packages/core/src/Logic/Prover.ts b/packages/core/src/Logic/Prover.ts index b09e38d4..7c8e7c6a 100644 --- a/packages/core/src/Logic/Prover.ts +++ b/packages/core/src/Logic/Prover.ts @@ -1,9 +1,11 @@ import { + type TruthValue, And, Atom, Formula, Or, evaluate, + hasUndecidable, negate, properties, } from '../Formula.js' @@ -35,20 +37,20 @@ export default class Prover< PropertyId >, > { - private traits: Map + private traits: Map private derivations: Derivations private queue: Queue constructor( implications: ImplicationIndex, - traits = new Map(), + traits = new Map(), ) { this.traits = traits this.derivations = new Derivations([...traits.keys()]) this.queue = new Queue(implications) - traits.forEach((_: boolean, id: PropertyId) => { + traits.forEach((_: TruthValue, id: PropertyId) => { this.queue.mark(id) }) } @@ -95,7 +97,7 @@ export default class Prover< ]) } else if (av === true) { return this.force(implication.id, c, [...properties(a)]) - } else if (cv === false) { + } else if (cv === false && !hasUndecidable(a)) { return this.force(implication.id, negate(a), [...properties(c)]) } } @@ -114,16 +116,39 @@ export default class Prover< ): Contradiction | undefined { const property = formula.property - if (this.traits.has(property)) { - if (this.traits.get(property) !== formula.value) { - return this.contradiction(theorem, [...support, property]) - } else { + const existing = this.traits.get(property) + + if (existing !== undefined) { + if (existing === formula.value) { + return + } + // undecidable has lower priority: true/false overrides it + if (existing === 'undecidable' && formula.value !== 'undecidable') { + this.traits.set(property, formula.value as TruthValue) + this.derivations.overrideGiven(property) + this.derivations.addEvidence( + property, + formula.value as TruthValue, + theorem, + support, + ) + this.queue.mark(property) return } + // don't let undecidable override a definite value + if (formula.value === 'undecidable') { + return + } + return this.contradiction(theorem, [...support, property]) } - this.traits.set(property, formula.value) - this.derivations.addEvidence(property, formula.value, theorem, support) + this.traits.set(property, formula.value as TruthValue) + this.derivations.addEvidence( + property, + formula.value as TruthValue, + theorem, + support, + ) this.queue.mark(property) } diff --git a/packages/core/src/Logic/index.ts b/packages/core/src/Logic/index.ts index 88d2d015..27bb7509 100644 --- a/packages/core/src/Logic/index.ts +++ b/packages/core/src/Logic/index.ts @@ -2,7 +2,7 @@ export { default as ImplicationIndex } from './ImplicationIndex.js' export { Derivations } from './Derivations.js' export { Contradiction, Proof } from './Prover.js' -import { Formula, negate } from '../Formula.js' +import { type TruthValue, Formula, hasUndecidable, negate } from '../Formula.js' import ImplicationIndex from './ImplicationIndex.js' import Prover, { Contradiction, Proof, Result } from './Prover.js' import { Id } from './Types.js' @@ -11,7 +11,7 @@ import { Id } from './Types.js' // find either the collection of derivable traits, or a contradiction export function deduceTraits( implications: ImplicationIndex, - traits: Map, + traits: Map, ): Result { return new Prover(implications, traits).run() } @@ -71,14 +71,16 @@ export function proveTheorem( return formatProof(result.contradiction) } - contradiction = prover.force('given', negate(then)) - if (contradiction) { - return formatProof(contradiction) - } + if (!hasUndecidable(then)) { + contradiction = prover.force('given', negate(then)) + if (contradiction) { + return formatProof(contradiction) + } - result = prover.run() - if (result.kind === 'contradiction') { - return formatProof(result.contradiction) + result = prover.run() + if (result.kind === 'contradiction') { + return formatProof(result.contradiction) + } } } diff --git a/packages/core/src/Trait.ts b/packages/core/src/Trait.ts index a9188ed9..12a68f28 100644 --- a/packages/core/src/Trait.ts +++ b/packages/core/src/Trait.ts @@ -1,5 +1,6 @@ import { z } from 'zod' import { Id as BaseId } from './Id.js' +import { type TruthValue } from './Formula.js' import { Record, recordSchema } from './Record.js' export const proofSchema = (id: z.ZodSchema): z.ZodSchema> => @@ -18,7 +19,7 @@ export const traitSchema = (id: z.ZodSchema): z.ZodSchema> => z.object({ space: id, property: id, - value: z.boolean(), + value: z.union([z.boolean(), z.literal('undecidable')]), proof: proofSchema(id).optional(), }), recordSchema, @@ -27,6 +28,6 @@ export const traitSchema = (id: z.ZodSchema): z.ZodSchema> => export type Trait = Record & { space: Id property: Id - value: boolean + value: TruthValue proof?: Proof } diff --git a/packages/core/src/index.ts b/packages/core/src/index.ts index bb346fae..280efce3 100644 --- a/packages/core/src/index.ts +++ b/packages/core/src/index.ts @@ -5,7 +5,13 @@ import { theoremSchema } from './Theorem.js' import { traitSchema } from './Trait.js' export { type Bundle } from './Bundle.js' -export { type Formula, type And, type Atom, type Or } from './Formula.js' +export { + type Formula, + type And, + type Atom, + type Or, + type TruthValue, +} from './Formula.js' export { parser } from './Parser.js' export { type Property, PropertyPage } from './Property.js' export { diff --git a/packages/viewer/src/components/Shared/Formula/Atom.svelte b/packages/viewer/src/components/Shared/Formula/Atom.svelte index ff37fe10..e9fd64de 100644 --- a/packages/viewer/src/components/Shared/Formula/Atom.svelte +++ b/packages/viewer/src/components/Shared/Formula/Atom.svelte @@ -8,6 +8,12 @@ export let link: boolean = true -{value.value === null ? '?' : value.value ? '' : '¬'}{#if link}{:else}{/if} +{value.value === null + ? '?' + : value.value === 'undecidable' + ? '⊬' + : value.value + ? '' + : '¬'}{#if link}{:else}{/if} diff --git a/packages/viewer/src/components/Traits/FilterButtons.svelte b/packages/viewer/src/components/Traits/FilterButtons.svelte index a3531b1e..c571ca80 100644 --- a/packages/viewer/src/components/Traits/FilterButtons.svelte +++ b/packages/viewer/src/components/Traits/FilterButtons.svelte @@ -46,6 +46,17 @@ > +