Efficient Statement

Efficient statement handling for geometric theorem proving.

This module provides data structures and utilities for representing and manipulating geometric statements in a theorem proving system. It includes:

Named tuple classes for different types of geometric statements (perpendicular, parallel, equal angles, etc.)
Named tuple classes for corresponding predicates with variable names
Functions for generating permutations of statements based on geometric symmetries
Functions for normalizing statements to canonical forms
Utilities for finding representatives of equivalence classes

The module is designed for efficiency in geometric theorem proving by providing canonical representations and symmetry handling for geometric statements.

efficient_version(predicate)

Return type:: Union[PerpStatement, ParaStatement, EqangleStatement, EqratioStatement, CongStatement, MidptStatement, CollStatement, CircleStatement, TriangleStatement, CyclicStatement]

class PerpStatement(name, a, b, c, d)

Bases: NamedTuple

Create new instance of PerpStatement(name, a, b, c, d)

name: Literal['perp']: Alias for field number 0

a: NewType(PredicateArgument, str): Alias for field number 1

b: NewType(PredicateArgument, str): Alias for field number 2

c: NewType(PredicateArgument, str): Alias for field number 3

d: NewType(PredicateArgument, str): Alias for field number 4

class PerpPredicate(name, A, B, C, D)

Bases: NamedTuple

Create new instance of PerpPredicate(name, A, B, C, D)

name: Literal['perp']: Alias for field number 0

A: NewType(VarName, str): Alias for field number 1

B: NewType(VarName, str): Alias for field number 2

C: NewType(VarName, str): Alias for field number 3

D: NewType(VarName, str): Alias for field number 4

class ParaStatement(name, a, b, c, d)

Bases: NamedTuple

Create new instance of ParaStatement(name, a, b, c, d)

name: Literal['para']: Alias for field number 0

a: NewType(PredicateArgument, str): Alias for field number 1

b: NewType(PredicateArgument, str): Alias for field number 2

c: NewType(PredicateArgument, str): Alias for field number 3

d: NewType(PredicateArgument, str): Alias for field number 4

class ParaPredicate(name, A, B, C, D)

Bases: NamedTuple

Create new instance of ParaPredicate(name, A, B, C, D)

name: Literal['para']: Alias for field number 0

A: NewType(VarName, str): Alias for field number 1

B: NewType(VarName, str): Alias for field number 2

C: NewType(VarName, str): Alias for field number 3

D: NewType(VarName, str): Alias for field number 4

class EqangleStatement(name, a, b, c, d, e, f, g, h)

Bases: NamedTuple

Create new instance of EqangleStatement(name, a, b, c, d, e, f, g, h)

name: Literal['eqangle']: Alias for field number 0

a: NewType(PredicateArgument, str): Alias for field number 1

b: NewType(PredicateArgument, str): Alias for field number 2

c: NewType(PredicateArgument, str): Alias for field number 3

d: NewType(PredicateArgument, str): Alias for field number 4

e: NewType(PredicateArgument, str): Alias for field number 5

f: NewType(PredicateArgument, str): Alias for field number 6

g: NewType(PredicateArgument, str): Alias for field number 7

h: NewType(PredicateArgument, str): Alias for field number 8

class EqanglePredicate(name, A, B, C, D, E, F, G, H)

Bases: NamedTuple

Create new instance of EqanglePredicate(name, A, B, C, D, E, F, G, H)

name: Literal['eqangle']: Alias for field number 0

A: NewType(VarName, str): Alias for field number 1

B: NewType(VarName, str): Alias for field number 2

C: NewType(VarName, str): Alias for field number 3

D: NewType(VarName, str): Alias for field number 4

E: NewType(VarName, str): Alias for field number 5

F: NewType(VarName, str): Alias for field number 6

G: NewType(VarName, str): Alias for field number 7

H: NewType(VarName, str): Alias for field number 8

class EqratioStatement(name, a, b, c, d, e, f, g, h)

Bases: NamedTuple

Create new instance of EqratioStatement(name, a, b, c, d, e, f, g, h)

name: Literal['eqratio']: Alias for field number 0

a: NewType(PredicateArgument, str): Alias for field number 1

b: NewType(PredicateArgument, str): Alias for field number 2

c: NewType(PredicateArgument, str): Alias for field number 3

d: NewType(PredicateArgument, str): Alias for field number 4

e: NewType(PredicateArgument, str): Alias for field number 5

f: NewType(PredicateArgument, str): Alias for field number 6

g: NewType(PredicateArgument, str): Alias for field number 7

h: NewType(PredicateArgument, str): Alias for field number 8

class EqratioPredicate(name, A, B, C, D, E, F, G, H)

Bases: NamedTuple

Create new instance of EqratioPredicate(name, A, B, C, D, E, F, G, H)

name: Literal['eqratio']: Alias for field number 0

A: NewType(VarName, str): Alias for field number 1

B: NewType(VarName, str): Alias for field number 2

C: NewType(VarName, str): Alias for field number 3

D: NewType(VarName, str): Alias for field number 4

E: NewType(VarName, str): Alias for field number 5

F: NewType(VarName, str): Alias for field number 6

G: NewType(VarName, str): Alias for field number 7

H: NewType(VarName, str): Alias for field number 8

class CongStatement(name, a, b, c, d)

Bases: NamedTuple

Create new instance of CongStatement(name, a, b, c, d)

name: Literal['cong']: Alias for field number 0

a: NewType(PredicateArgument, str): Alias for field number 1

b: NewType(PredicateArgument, str): Alias for field number 2

c: NewType(PredicateArgument, str): Alias for field number 3

d: NewType(PredicateArgument, str): Alias for field number 4

class CongPredicate(name, A, B, C, D)

Bases: NamedTuple

Create new instance of CongPredicate(name, A, B, C, D)

name: Literal['cong']: Alias for field number 0

A: NewType(VarName, str): Alias for field number 1

B: NewType(VarName, str): Alias for field number 2

C: NewType(VarName, str): Alias for field number 3

D: NewType(VarName, str): Alias for field number 4

class MidptStatement(name, a, b, c)

Bases: NamedTuple

Create new instance of MidptStatement(name, a, b, c)

name: Literal['midp']: Alias for field number 0

a: NewType(PredicateArgument, str): Alias for field number 1

b: NewType(PredicateArgument, str): Alias for field number 2

c: NewType(PredicateArgument, str): Alias for field number 3

class MidptPredicate(name, A, B, C)

Bases: NamedTuple

Create new instance of MidptPredicate(name, A, B, C)

name: Literal['midp']: Alias for field number 0

A: NewType(VarName, str): Alias for field number 1

B: NewType(VarName, str): Alias for field number 2

C: NewType(VarName, str): Alias for field number 3

class TriangleStatement(name, a, b, c, p, q, r)

Bases: NamedTuple

Create new instance of TriangleStatement(name, a, b, c, p, q, r)

name: Literal['simtri', 'simtrir', 'contri', 'contrir']: Alias for field number 0

a: NewType(PredicateArgument, str): Alias for field number 1

b: NewType(PredicateArgument, str): Alias for field number 2

c: NewType(PredicateArgument, str): Alias for field number 3

p: NewType(PredicateArgument, str): Alias for field number 4

q: NewType(PredicateArgument, str): Alias for field number 5

r: NewType(PredicateArgument, str): Alias for field number 6

class TrianglePredicate(name, A, B, C, P, Q, R)

Bases: NamedTuple

Create new instance of TrianglePredicate(name, A, B, C, P, Q, R)

name: Literal['simtri', 'simtrir', 'contri', 'contrir']: Alias for field number 0

A: NewType(VarName, str): Alias for field number 1

B: NewType(VarName, str): Alias for field number 2

C: NewType(VarName, str): Alias for field number 3

P: NewType(VarName, str): Alias for field number 4

Q: NewType(VarName, str): Alias for field number 5

R: NewType(VarName, str): Alias for field number 6

class CollStatement(predicate_name: str, *points: str): Bases: tuple[str, …]

class CollPredicate(predicate_name: str, *points: str): Bases: tuple[str, …]

class CircleStatement(predicate_name: str, *points: str): Bases: tuple[str, …]

class CirclePredicate(predicate_name: str, *points: str): Bases: tuple[str, …]

class CyclicStatement(predicate_name: str, *points: str): Bases: tuple[str, …]

class CyclicPredicate(predicate_name: str, *points: str): Bases: tuple[str, …]

generate_permutations(stmt)

Return type:: Iterator[Union[PerpStatement, ParaStatement, EqangleStatement, EqratioStatement, CongStatement, MidptStatement, CollStatement, CircleStatement, TriangleStatement, CyclicStatement]]

cyclic_perms(stmt)

Return type:: Iterator[CyclicStatement]

coll_perms(stmt)

Return type:: Iterator[CollStatement]

circle_perms(stmt)

Return type:: Iterator[CircleStatement]

triangle_perms(stmt)

Return type:: Iterator[TriangleStatement]

normalize_triangle(stmt_pts)

Return type:: TriangleStatement

normalize_midpt(stmt_pts)

Return type:: MidptStatement

midpt_perms(stmt_pts)

Return type:: Iterator[MidptStatement]

normalize_cong(stmt_pts)

Return type:: CongStatement

cong_perms(stmt_pts)

Return type:: Iterator[CongStatement]

normalize_eqratio(stmt_pts)

Return type:: EqratioStatement

eqratio_perms(stmt_pts)

Return type:: Iterator[EqratioStatement]

normalize_eqangle(stmt_pts)

Return type:: EqangleStatement

eqangle_perms(stmt_pts)

Return type:: Iterator[EqangleStatement]

normalize_para(stmt_pts)

Return type:: ParaStatement

para_perms(stmt_pts)

Return type:: Iterator[ParaStatement]

normalize_perp(stmt_pts)

Return type:: PerpStatement

perp_perms(stmt_pts)

Return type:: Iterator[PerpStatement]

normalize_coll(stmt_pts)

Return type:: CollStatement

normalize_circle(stmt_pts)

Return type:: CircleStatement

normalize_cyclic(stmt_pts)

Return type:: CyclicStatement

get_representative_of_equivalence_class(stmt)

Return type:: Union[PerpStatement, ParaStatement, EqangleStatement, EqratioStatement, CongStatement, MidptStatement, CollStatement, CircleStatement, TriangleStatement, CyclicStatement]