Conjecture

A Conjecture packages a row‐wise logical implication

\[H(x)\;\Longrightarrow\;C(x)\]

where H (the hypothesis) and C (the conclusion) are both Predicate objects. It provides:

  • Deferred evaluation: calling conj(df) returns a Boolean mask

  • Universal check: conj.is_true(df) tells you if it holds on every row

  • Accuracy, counterexamples, and integration into discovery pipelines

Creation Methods

There are three equivalent ways to build a Conjecture(H, C):

  1. Direct constructor

  2. `.implies(…, as_conjecture=True)`

  3. Shift operator `>>`

Below we illustrate all three.

import pandas as pd
from txgraffiti.logic.conjecture_logic import (
    Property, Predicate, Conjecture, TRUE
)

# Sample DataFrame
df = pd.DataFrame({
    'alpha':    [1, 2, 3],
    'beta':     [3, 1, 1],
    'connected':[True, True, True],
    'tree':     [False, False, True],
})

# Lift numeric columns to Property
alpha = Property('alpha',   lambda df: df['alpha'])
beta  = Property('beta',    lambda df: df['beta'])

# Hypothesis and conclusion
hypothesis = Predicate('connected', lambda df: df['connected'])
conclusion = alpha <= (2 * beta + 3)

# 1) Direct constructor
conj1 = Conjecture(hypothesis, conclusion)
print(f"conj1 = {conj1}")
print(conj1(df))
print(f"conj1.is_true(df) = {conj1.is_true(df)}\n")

# 2) Using .implies(..., as_conjecture=True)
conj2 = hypothesis.implies(conclusion, as_conjecture=True)
print(f"conj2 = {conj2}")
print(conj2(df))
print(f"conj2.is_true(df) = {conj2.is_true(df)}\n")

# 3) Using >> operator
conj3 = hypothesis >> conclusion
print(f"conj3 = {conj3}")
print(conj3(df))
print(f"conj3.is_true(df) = {conj3.is_true(df)}\n")

# Expected output:

conj1 = <Conj (connected) → (alpha <= ((2 * beta) + 3))>
0    True
1    True
2    True
dtype: bool
conj1.is_true(df) = True

conj2 = <Conj (connected) → (alpha <= ((2 * beta) + 3))>
0    True
1    True
2    True
dtype: bool
conj2.is_true(df) = True

conj3 = <Conj (connected) → (alpha <= ((2 * beta) + 3))>
0    True
1    True
2    True
dtype: bool
conj3.is_true(df) = True

Key Methods

  • `conj(df)` Returns a pandas.Series[bool] mask equal to ((¬H(df)) ∨ C(df)).

  • `conj.is_true(df)` Returns True iff every row satisfies the implication.

  • `conj.accuracy(df)` Fraction of rows where H is true that also satisfy C.

  • `conj.counterexamples(df)` Returns a DataFrame of rows violating the implication.

Integration

Conjecture objects can be:

  • Filtered by heuristics (e.g. Morgan, Dalmatian)

  • Sorted or deduplicated in post‐processors

  • Exported to formal‐proof stubs (Lean 4) via export_to_lean

Use Conjecture as the core unit in your automated‐discovery workflows.