import Type, { type Static } from "typebox";
export declare const CorePropositionalExpressionTypes: Type.TUnion<[Type.TLiteral<"variable">, Type.TLiteral<"operator">, Type.TLiteral<"formula">]>;
export type TCorePropositionalExpressionTypes = Static<typeof CorePropositionalExpressionTypes>;
export declare const CorePropositionalVariableExpressionSchema: Type.TObject<{
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    premiseId: Type.TString;
    parentId: Type.TUnion<[Type.TString, Type.TNull]>;
    position: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    type: Type.TLiteral<"variable">;
    variableId: Type.TString;
    enthymeme: Type.TOptional<Type.TLiteral<true>>;
}>;
export type TCorePropositionalVariableExpression = Static<typeof CorePropositionalVariableExpressionSchema>;
export declare const CoreLogicalOperatorType: Type.TUnion<[Type.TLiteral<"not">, Type.TLiteral<"and">, Type.TLiteral<"or">, Type.TLiteral<"xor">, Type.TLiteral<"implies">, Type.TLiteral<"iff">]>;
export type TCoreLogicalOperatorType = Static<typeof CoreLogicalOperatorType>;
export declare const CoreOperatorExpressionSchema: Type.TObject<{
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    premiseId: Type.TString;
    parentId: Type.TUnion<[Type.TString, Type.TNull]>;
    position: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    type: Type.TLiteral<"operator">;
    operator: Type.TUnion<[Type.TLiteral<"not">, Type.TLiteral<"and">, Type.TLiteral<"or">, Type.TLiteral<"xor">, Type.TLiteral<"implies">, Type.TLiteral<"iff">]>;
}>;
export type TCoreOperatorExpression = Static<typeof CoreOperatorExpressionSchema>;
export declare const CoreFormulaExpressionSchema: Type.TObject<{
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    premiseId: Type.TString;
    parentId: Type.TUnion<[Type.TString, Type.TNull]>;
    position: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    type: Type.TLiteral<"formula">;
}>;
export type TCoreFormulaExpression = Static<typeof CoreFormulaExpressionSchema>;
export declare const CorePropositionalExpressionSchema: Type.TUnion<[Type.TObject<{
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    premiseId: Type.TString;
    parentId: Type.TUnion<[Type.TString, Type.TNull]>;
    position: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    type: Type.TLiteral<"variable">;
    variableId: Type.TString;
    enthymeme: Type.TOptional<Type.TLiteral<true>>;
}>, Type.TObject<{
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    premiseId: Type.TString;
    parentId: Type.TUnion<[Type.TString, Type.TNull]>;
    position: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    type: Type.TLiteral<"operator">;
    operator: Type.TUnion<[Type.TLiteral<"not">, Type.TLiteral<"and">, Type.TLiteral<"or">, Type.TLiteral<"xor">, Type.TLiteral<"implies">, Type.TLiteral<"iff">]>;
}>, Type.TObject<{
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    premiseId: Type.TString;
    parentId: Type.TUnion<[Type.TString, Type.TNull]>;
    position: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    type: Type.TLiteral<"formula">;
}>]>;
export type TCorePropositionalExpressionCombined = Static<typeof CorePropositionalExpressionSchema>;
export type TCorePropositionalExpression<T extends TCorePropositionalExpressionTypes = TCorePropositionalExpressionTypes> = Extract<TCorePropositionalExpressionCombined, {
    type: T;
}>;
export declare const CoreClaimBoundVariableSchema: Type.TObject<{
    claimId: Type.TString;
    claimVersion: Type.TNumber;
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    symbol: Type.TString;
    checksum: Type.TString;
}>;
export type TClaimBoundVariable = Static<typeof CoreClaimBoundVariableSchema>;
export declare const CorePremiseBoundVariableSchema: Type.TObject<{
    boundPremiseId: Type.TString;
    boundArgumentId: Type.TString;
    boundArgumentVersion: Type.TNumber;
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    symbol: Type.TString;
    checksum: Type.TString;
}>;
export type TPremiseBoundVariable = Static<typeof CorePremiseBoundVariableSchema>;
export declare const CorePropositionalVariableSchema: Type.TUnion<[Type.TObject<{
    claimId: Type.TString;
    claimVersion: Type.TNumber;
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    symbol: Type.TString;
    checksum: Type.TString;
}>, Type.TObject<{
    boundPremiseId: Type.TString;
    boundArgumentId: Type.TString;
    boundArgumentVersion: Type.TNumber;
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    symbol: Type.TString;
    checksum: Type.TString;
}>]>;
export type TCorePropositionalVariable = Static<typeof CorePropositionalVariableSchema>;
/** Type guard: returns `true` if the variable is claim-bound. */
export declare function isClaimBound(v: TCorePropositionalVariable): v is TClaimBoundVariable;
/** Type guard: returns `true` if the variable is premise-bound. */
export declare function isPremiseBound(v: TCorePropositionalVariable): v is TPremiseBoundVariable;
/** Returns `true` if the premise-bound variable references a premise in a different argument. */
export declare function isExternallyBound(v: TPremiseBoundVariable, argumentId: string): boolean;
export declare const CoreFreeformPremiseSchema: Type.TObject<{
    type: Type.TLiteral<"freeform">;
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    enthymeme: Type.TOptional<Type.TLiteral<true>>;
}>;
export declare const CoreDerivationPremiseSchema: Type.TObject<{
    type: Type.TLiteral<"derivation">;
    derivedClaimId: Type.TString;
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    enthymeme: Type.TOptional<Type.TLiteral<true>>;
}>;
export declare const CorePremiseSchema: Type.TUnion<[Type.TObject<{
    type: Type.TLiteral<"freeform">;
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    enthymeme: Type.TOptional<Type.TLiteral<true>>;
}>, Type.TObject<{
    type: Type.TLiteral<"derivation">;
    derivedClaimId: Type.TString;
    id: Type.TString;
    argumentId: Type.TString;
    argumentVersion: Type.TNumber;
    checksum: Type.TString;
    descendantChecksum: Type.TUnion<[Type.TString, Type.TNull]>;
    combinedChecksum: Type.TString;
    enthymeme: Type.TOptional<Type.TLiteral<true>>;
}>]>;
export type TCoreFreeformPremise = Static<typeof CoreFreeformPremiseSchema>;
export type TCoreDerivationPremise = Static<typeof CoreDerivationPremiseSchema>;
export type TCorePremise = Static<typeof CorePremiseSchema>;
//# sourceMappingURL=propositional.d.ts.map