core/src/Logic/Prover.test.ts at 34576cd1fe3d28cb347deadaa18956817b8c9fb4 · pi-base/core · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
import { and, atom, or } from '../Formula'
import { Contradiction, Derivation, deduceTraits, proveTheorem } from './Prover'
import ImplicationIndex from './ImplicationIndex'
import { index, recordToMap } from '../__test__'

describe('deduceTraits', () => {
  let contradiction: Contradiction<number> | undefined
  let deductions: Derivation<number>[]

  beforeEach(() => {
    contradiction = undefined
    deductions = []
  })

  function run(
    theorems: ImplicationIndex<number>,
    traits: Record<string, boolean>
  ): void {
    const result = deduceTraits(theorems, recordToMap(traits))
    if (result.kind === 'contradiction') {
      contradiction = result.contradiction
    } else {
      deductions = result.derivations.all()
    }
  }

  const theorems = index(
    [atom('P'), atom('Q')],
    [atom('Q'), atom('R')],
    [atom('R'), or(atom('S'), atom('T'))],
    [and(atom('X'), atom('Y')), atom('T', false)]
  )

  describe('chained proofs', () => {
    beforeEach(() => {
      run(theorems, {
        P: true,
        S: false,
        X: true,
      })
    })

    it('does not find a contradiction', () => {
      expect(contradiction).toBeUndefined()
    })

    it('proves the expected traits', () => {
      expect(deductions).toEqual([
        {
          property: 'Q',
          value: true,
          proof: { properties: ['P'], theorems: [1] },
        },
        {
          property: 'R',
          value: true,
          proof: { properties: ['P'], theorems: [2, 1] },
        },
        {
          property: 'T',
          value: true,
          proof: { properties: ['S', 'P'], theorems: [3, 2, 1] },
        },
        {
          property: 'Y',
          value: false,
          proof: { properties: ['X', 'S', 'P'], theorems: [4, 3, 2, 1] },
        },
      ])
    })
  })
})

describe('proveTheorem', () => {
  const theorems = index(
    [and(atom('P'), atom('Q')), atom('R')],
    [atom('R'), atom('P')],
    [atom('R'), atom('S')],
    [atom('S'), atom('Q')]
  )

  it('can find a chained proof', () => {
    const proof = proveTheorem(theorems, atom('R'), atom('Q'))

    expect(proof).toEqual([4, 3])
  })

  it('can identify a tautology', () => {
    const proof = proveTheorem(index(), atom('P'), atom('P'))

    expect(proof).toEqual('tautology')
  })

  it('can fail to find a proof', () => {
    const proof = proveTheorem(theorems, atom('P'), atom('P', false))

    expect(proof).toBeUndefined()
  })
})