import type { TViolation } from "../types.js";
import type { TValidatorContext } from "./context.js";
/**
 * P-1 — Formula buffer between operators. A non-`not` operator (`and`,
 * `or`, `xor`, `implies`, `iff`) is never a direct child of another operator
 * expression. `not` is exempt — it can be a direct child of any
 * operator.
 *
 * Reports the inner (child) operator that breaks the rule, with the
 * outer (parent) operator referenced in the message.
 */
export declare function validateP1(ctx: TValidatorContext): readonly TViolation[];
/**
 * P-2 — No double negation. `not(not(x))` does not appear in the tree.
 * Reports the outer NOT.
 */
export declare function validateP2(ctx: TValidatorContext): readonly TViolation[];
/**
 * P-3 — Formula has operator descendant. A `formula` node's bounded
 * subtree (stopping at the next nested formula) contains at least one
 * variadic connective (`and`, `or` or `xor`). Formulas wrapping a leaf or
 * a single `not` chain are not Presentable.
 */
export declare function validateP3(ctx: TValidatorContext): readonly TViolation[];
/**
 * P-4 — No single-child variadic operator. `and` / `or` / `xor` with
 * exactly one child is not Presentable. Largely redundant with E-1
 * (variadic arity ≥ 2), kept for clarity in the rule inventory.
 */
export declare function validateP4(ctx: TValidatorContext): readonly TViolation[];
/**
 * P-5 — No operator-of-same-type adjacency through a formula. When a
 * parent operator (`and` / `or` / `xor`) has a `formula` child whose only
 * descendant operator (after peeling through transparent formula
 * buffers) is the same operator, the inner operator should be absorbed
 * into the parent.
 *
 * Example: `AND(formula(AND(b, c)), d)` should be `AND(b, c, d)`.
 *
 * The rule applies to the variadic connectives only — `implies` / `iff`
 * are root-only per S-5 and cannot appear as a child operator, and `not`
 * is unary so there is nothing to absorb.
 */
export declare function validateP5(ctx: TValidatorContext): readonly TViolation[];
/**
 * P-6 — An enthymeme marks a claim-bound variable. An expression carrying
 * `enthymeme: true` is a variable expression, and its variable is claim-bound.
 *
 * The TypeScript types confine the annotation to variable expressions and
 * premises, but the entity schemas stay open for app-level fields, so a mark
 * on an operator or formula expression is reachable through the library API
 * and shifts that expression's checksum. Both halves are reported here because
 * neither is expressible in the schema: an operator has no assertion to
 * suppress, and claim-boundness is a property of the variable an expression
 * points at rather than of the expression itself. Marking a premise-bound
 * variable is meaningless in the same way — its truth is derived from another
 * premise's evaluation, so there is no natural-language assertion a speaker
 * could have left out.
 *
 * An expression whose variable cannot be resolved is not reported here; the
 * dangling reference is a Structural concern.
 */
export declare function validateP6(ctx: TValidatorContext): readonly TViolation[];
export declare function validatePresentable(ctx: TValidatorContext): readonly TViolation[];
//# sourceMappingURL=presentable.d.ts.map