/**
   * Represents a set of propositional variables.
   */
type PropositionalVariable = 'A' | 'B' | 'C' | 'D' | 'E' | 'F' | 'G' | 'H' | 'I' | 'J' | 'K' | 'L' | 'M' | 'N' | 'O' | 'P' | 'Q' | 'R' | 'S' | 'T' | 'U' | 'V' | 'W' | 'X' | 'Y' | 'Z';

/**
   * Represents a generic unary operation.
   * @interface UnaryOperation
   */
interface UnaryOperation {
    /**
       * The type of the unary operation.
       */
    operation: string;
    /**
       * The formula associated with the unary operation.
       */
    value: Formula;
}
/**
   * Represents a unary operation of type Negation (¬).
   * @interface Negation
   * @extends {UnaryOperation}
   */
interface Negation extends UnaryOperation {
    readonly operation: 'Negation';
}

/**
   * Represents a generic binary operation.
   * @interface BinaryOperation
   */
interface BinaryOperation {
    /**
       * The type of the binary operation.
       */
    operation: string;
    /**
       * The formula on the right side of the binary operation.
       */
    right: Formula;
    /**
       * The formula on the left side of the binary operation.
       */
    left: Formula;
}
/**
   * Represents a binary operation of type Biconditional (<->).
   * @interface Biconditional
   * @extends {BinaryOperation}
   */
interface Biconditional extends BinaryOperation {
    readonly operation: 'Biconditional';
}
/**
   * Represents a binary operation of type Conjunction (∧).
   * @interface Conjunction
   * @extends {BinaryOperation}
   */
interface Conjunction extends BinaryOperation {
    readonly operation: 'Conjunction';
}
/**
   * Represents a binary operation of type Disjunction (∨).
   * @interface Disjunction
   * @extends {BinaryOperation}
   */
interface Disjunction extends BinaryOperation {
    readonly operation: 'Disjunction';
}
/**
   * Represents a binary operation of type Implication (->).
   * @interface Implication
   * @extends {BinaryOperation}
   */
interface Implication extends BinaryOperation {
    readonly operation: 'Implication';
}

/**
   * Represents a generic logical formula.
   */
type Formula = PropositionalVariable | Negation | Conjunction | Disjunction | Implication | Biconditional;

/**
   * List of available inference rules.
   */
declare const INFERENCE_RULES: readonly ["Associativity (Biconditional)", "Associativity (Conjunction)", "Associativity (Disjunction)", "Biconditional Elimination", "Biconditional Introduction", "Commutativity", "Conditional Proof", "Conditionalization", "Contraposition", "Conjunction Elimination", "Conjunction Introduction", "Contraposition", "De Morgan", "Disjunction Introduction", "Disjunctive Syllogism", "Distribution (Conjunction over Disjunction)", "Distribution (Disjunction over Conjunction)", "Double Negation", "Double Negation Introduction", "Hypothetical Syllogism", "Implication Elimination", "Implication Negation", "Modus Ponens", "Modus Tollens", "Reductio Ad Absurdum"];
/**
   * Represents the types of items in a proof.
   */
type ProofItemType = 'Premise' | 'Hypothesis' | 'Knowledge' | 'Conclusion' | 'End of Hypothesis';
type InferenceRule = typeof INFERENCE_RULES[number];
/**
   * Represents the base structure of a proof item.
   */
interface ProofItemBase {
    /**
       * The unique identifier of the proof item.
       */
    id: number;
    /**
       * The type of the proof item.
       */
    type: ProofItemType;
    /**
       * The logical expression associated with the proof item.
       */
    expression: string | Formula;
}
/**
   * Represents an inferred proof item.
   */
interface ProofItemInferred extends ProofItemBase {
    type: 'Knowledge' | 'Conclusion' | 'End of Hypothesis';
    /**
       * The source of the inference, including the line numbers and the inference rule applied.
       * @example
      * // This indicates that the proof item is inferred from lines 1 and 2 using the 'Conjunction Introduction' rule.
       * from: [[1, 2], 'Conjunction Introduction']
       */
    from: [number[], InferenceRule];
}
/**
   * Represents the end of a hypothesis in a proof.
   */
interface ProofEndOfHypothesis extends ProofItemInferred {
    type: 'End of Hypothesis';
    hypothesisId: number;
}
type ProofItem = ProofItemBase | ProofItemInferred | ProofEndOfHypothesis;
/**
   * Represents a proof as a mapping of item IDs to proof items.
   * @example
   * const proof: Proof = {
   *   1: {
   *     id: 1,
   *     type: 'Premisse',
   *     expression: 'P',
   *   },
   *   2: {
   *     id: 2,
   *     type: 'Premisse',
   *     expression: 'P -> Q',
   *   },
   *   3: {
   *     id: 3,
   *     expression: 'Q',
   *     type: 'Conclusion',
   *     from: [[1, 2], 'Modus Ponens'],
   *   },
   * };
   */
type Proof = Record<number, ProofItem>;
/**
   * Represents a mapped proof as a mapping of item IDs to proof items with scope information.
   */
type MappedProof = Record<number, ProofItem & {
    scopeIdx: number[];
}>;
/**
   * A mapping of inference rules to functions that apply the rules to proof items.
   */
declare const inferenceRulesMap: Record<InferenceRule, (proofItem: ProofItem, proof: Proof) => Formula | Formula[]>;

/**
 * Represents logical operators used in propositional logic.
 *
 * - '¬' (Negation): Represents logical negation (NOT).
 * - '∧' (Conjunction): Represents logical conjunction (AND).
 * - '∨' (Disjunction): Represents logical disjunction (OR).
 * - '->' (Implication): Represents logical implication (IF...THEN).
 * - '<->' (Biconditional): Represents logical biconditional (IF AND ONLY IF).
 * - '!' (Negation, alternative symbol): Represents logical negation (NOT).
 * - '&' (Conjunction, alternative symbol): Represents logical conjunction (AND).
 * - '|' (Disjunction, alternative symbol): Represents logical disjunction (OR).
 */
type Operator = '¬' | '∧' | '∨' | '->' | '<->' | '!' | '&' | '|';
/**
   * Represents boundary characters used in propositional logic.
   */
type Boundary = '(' | ')';
/**
   * Represents the types of possible tokens in a formula.
   */
type TokenType = 'variable' | 'operator' | 'boundary';
/**
   * A map that associates token types with their corresponding values.
   * @property {PropositionalVariable} variable - Represents a propositional variable.
   * @property {Operator} operator - Represents a logical operator.
   * @property {Boundary} boundary - Represents a boundary character.
   */
type TokenMap = {
    variable: PropositionalVariable;
    operator: Operator;
    boundary: Boundary;
};
/**
   * Represents a token in a formula.
   * @property {TokenType} type - The type of the token.
   * @property {PropositionalVariable | Operator | Boundary} value - The value of the token.
   * @example
   * const token: Token = { type: 'variable', value: 'P' };
   */
type Token = {
    [K in keyof TokenMap]: {
        type: K;
        value: TokenMap[K];
    };
}[keyof TokenMap];

type TruthValue = 0 | 1 | true | false;
/**
   * Represents a mapping of propositional variables to their truth values.
   */
type PropositionalVariableValues = {
    [K in PropositionalVariable]?: boolean;
};
/**
  * Represents a truth table containing headers, truth combinations, and truth values.
  *
  * @example
  * ```
  *  {
  *    headers: ['P', 'Q', '(P -> Q)'],
  *    truthCombinations: [
  *      [0, 0], [0, 1],
  *      [1, 0], [1, 1]
  *    ],
  *    truthValues: [true, true, false, true]
  * }
  * ```
  */
interface TruthTable {
    /**
     * An array of headers representing the variables and formula.
     *
     * @property {string[]}
     */
    headers: string[];
    /**
     * An array of arrays representing truth combinations for each variable.
     *
     * @property {TruthValue[][]}
     */
    truthCombinations: TruthValue[][];
    /**
     * An array of truth values representing the truth values for each combination.
     *
     * @property {TruthValue[]}
     */
    truthValues: TruthValue[];
}

type AtomicFormula = PropositionalVariable;

type MolecularFormula = Negation | Conjunction | Disjunction | Implication | Biconditional;

type BinaryOperationFormula = Conjunction | Disjunction | Implication | Biconditional;

/**
 * Class responsible for performing semantic truth-value operations, such as evaluate formulas and generate truth tables.
 */
declare class Calculator {
    /**
     * Generates a truth table for the given formula.
     *
     * @param formula - The logical formula to generate a truth table for.
     * @param stringfiedFormula - An optional string representation of the formula.
     * @returns The truth table as an array containing headers, truth combinations, and results.
     *
     * @example
     * const output = Calculator.generateTruthTable('P -> Q');
     * console.log(output);
     * // Output:
     * // {
     * //   headers: ['P', 'Q', '(P -> Q)'],
     * //   truthCombinations: [
     * //     [false, false], [false, true],
     * //     [true, false], [true, true]
     * //   ],
     * //   truthValues: [true, true, false, true]
     * // }
     */
    static generateTruthTable(formula: Formula | string, stringfiedFormula?: string): TruthTable;
    /**
     * Evaluates the given logical formula with the provided truth values for variables.
     *
     * @param formula - The logical formula to evaluate.
     * @param values - An object representing truth values for propositional variables.
     * @returns The result of the evaluation (true or false).
     *
     * @example
     * const result = Calculator.evaluate('P -> Q', { P: true, Q: false });
     * console.log(result); // Output: false
     */
    static evaluate<T extends Formula>(formula: T | string, values: PropositionalVariableValues): boolean;
    /**
     * Checks if a given formula is a semantic consequence of the given premises.
     * A semantic consequence holds if, in every possible truth assignment to the propositional variables,
     * when all premises are true, the conclusion is also true.
     *
     * @param premises - An array of logical formulas or strings representing the premises.
     * @param conclusion - The conclusion formula to check as a semantic consequence.
     * @returns True if the conclusion is a semantic consequence of the premises, false otherwise.
     *
     * @example
     * const output = Calculator.isSemanticConsequence(['P->Q', 'P'], 'Q');
     * console.log(output); // Output: true
     */
    static isSemanticConsequence(premises: Formula[] | string[], conclusion: Formula | string): boolean;
    private static evaluateImplication;
    private static evaluateBiconditional;
    private static evaluateConjunction;
    private static evaluateDisjunction;
    private static evaluateNegation;
    protected static generateTruthCombinations(numVariables: number): boolean[][];
    private static collectVariables;
}

/**
 * Class responsible for checking the syntactic validity of proofs.
 */
declare class ProofChecker {
    /**
     * Checks the given proof for validity.
     *
     * @param {Proof} proof - The proof to be checked.
     * @returns {boolean} - `true` if the proof is valid, `InferenceError` or `Error` otherwise.
     */
    static check(proof: Proof): boolean;
    /**
     * Creates a mapped version of the proof, with the representation of the scopes of each item.
     * @param {Proof} proof - The proof to be mapped.
     * @returns {MappedProof} - The mapped proof.
     */
    private static createMappedProof;
    /**
     * Validates the scope of inferred items.
     * @param {number[]} requiredItens - An array of required item IDs.
     * @param {ProofItemInferred} item - The inferred proof item to be validated.
     * @param {MappedProof} mappedProof - The mapped proof.
     */
    private static validateScope;
}

type ReducedFormula<T extends string | (BinaryOperation | Negation)> = T extends string ? string : T extends Implication ? Disjunction : T extends Biconditional ? Conjunction : T extends Conjunction ? Conjunction : T extends Disjunction ? Disjunction : T extends Negation ? Negation : never;

declare class Frege {
    private builder;
    private reducer;
    private calculator;
    private proofChecker;
    /**
     * The `parse` property provides functions to build and parse formulas in propositional logic.
     * @public
     */
    parse: {
        /**
         * Builds a formula object from a string, which contains a well-formed formula of the propositional logic.
         * @param formula - The logical formula to build.
         * @returns The built formula object.
         * @throws {UnrecognizedTokenException} If the provided formula contains unrecognized tokens.
         *
         * @example
         *
         * // Input: "P->Q"
         * // Output: { operation: 'Implication', left: 'P', right: 'Q' }
         * const parsedFormula = frege.parse.toFormulaObject<Implication>("P->Q");
         * console.log(parsedFormula);
         */
        toFormulaObject: <T extends Formula>(formula: string) => T;
        /**
         * Builds a logical formula string from a formula object using the syntax of propositional logic.
         * @param formula - The formula object to build the string from.
         * @returns The built logical formula string.
         * @throws {InvalidFormulaException} If the provided formula object is invalid or incomplete.
         *
         * @example
         *
         * // Input: { operation: 'Implication', left: 'P', right: 'Q' }
         * // Output: "(P->Q)"
         * const implication: Implication = {
         *    operation: 'Implication',
         *    left: 'P',
         *    right: 'Q'
         * };
         *
         * const parsedFormula = frege.parse.toFormulaString(implication);
         * console.log(parsedFormula); // => "(P->Q)"
         */
        toFormulaString: (formula: Formula) => string;
    };
    verifyConsequence: {
        semantic: typeof Calculator.isSemanticConsequence;
        syntactic: () => void;
    };
    /**
     * Reduces a formula object or a formula string to its reduced form.
     * @param formula - The formula object or formula string to reduce.
     * @returns The reduced formula in its string representation or as a formula object.
     *
     * @example
     * // Input: { operation: 'Implication', left: 'P', right: ' Q' }
     * // Output: { operation: 'Disjunction' left: { operation: 'Negation', value: 'P'}, right: 'Q' };
     *
     * const formulaObject: Implication = {
     *    operation: 'Implication',
     *    left: 'P',
     *    right: 'Q'
     * };
     *
     * const reducedFormula = frege.reduce(formulaObject);
     * console.log(reducedFormula); // => { operation: 'Disjunction' left: { operation: 'Negation', value: 'P'}, right: 'Q' };
     *
     *
     * // Input: "P<->Q"
     * // Output: '((¬(P) ∨ Q) ∧ (¬(Q) ∨ P))'
     *
     * const formulaString = "P<->Q";
     *
     * const reducedFormula = frege.reduce(formulaString);
     * console.log(reducedFormula); // => '((¬(P) ∨ Q) ∧ (¬(Q) ∨ P))'
     */
    reduce: <T extends string | Negation | BinaryOperationFormula>(formula: T) => ReducedFormula<T>;
    /**
     * Evaluates the given logical formula with the provided truth values for variables.
     *
     * @param formula - The logical formula to evaluate.
     * @param values - An object representing truth values for propositional variables.
     * @returns The result of the evaluation (true or false).
     *
     * @example
     * const result = Calculator.evaluate('P -> Q', { P: true, Q: false });
     * console.log(result); // Output: false
     */
    evaluate: typeof Calculator.evaluate;
    /**
     * Generates a truth table for the given formula.
     *
     * @param formula - The logical formula to generate a truth table for.
     * @param stringfiedFormula - An optional string representation of the formula.
     * @returns The truth table as an array containing headers, truth combinations, and results.
     *
     * @example
     * const output = Calculator.generateTruthTable('P -> Q');
     * console.log(output);
     * // Output:
     * {
     *    headers: ['P', 'Q', '(P -> Q)'],
     *    truthCombinations: [
     *      [false, false], [false, true],
     *      [true, false], [true, true]
     *    ],
     *    truthValues: [true, true, false, true]
     *  }
     */
    generateTruthTable: typeof Calculator.generateTruthTable;
    /**
     * Checks the given proof for validity.
     *
     * @param {Proof} proof - The proof to be checked.
     * @returns {boolean} - `true` if the proof is valid, `InferenceError` or `Error` otherwise.
     * @example
     * ```
     * const proof = {
      // ... (Your proof object)
      };
  
      const isProofValid = ProofChecker.check(proof);
      console.log(`The proof is valid: ${isProofValid}`);
     * ```
     */
    checkProof: typeof ProofChecker.check;
    /**
     * Checks if the given formula is a tautology.
     *
     * @param {Formula | string} formula - The formula to check.
     */
    isTautology: (formula: Formula | string) => boolean;
    /**
     * Checks if the given formula is a contradiction.
     *
     * @param {Formula | string} formula - The formula to check.
     */
    isContradiction: (formula: Formula | string) => boolean;
    /**
     * Checks if the given formula is a contingency.
     *
     * @param {Formula | string} formula - The formula to check.
     */
    isContingency: (formula: Formula | string) => boolean;
}

declare function isBiconditional(formula: any): formula is Biconditional;

declare function isConjunction(formula: any): formula is Conjunction;

declare function isDisjunction(formula: any): formula is Disjunction;

declare function isImplication(formula: any): formula is Implication;

declare function isContradiction(formula: Conjunction): boolean;

declare function isArrayString(array: Array<any>): array is string[];

declare function isBinaryOperationFormula(formula: any): formula is BinaryOperationFormula;

declare function isNegation(formula: any): formula is Negation;

declare function isHypothesis(x: ProofItem): boolean;

declare function isEndOfHypothesis(x: ProofItem): x is ProofEndOfHypothesis;

/**
 * Checks if the given formula is a molecular formula.
 * @param formula - The formula to check.
 * @returns True if the formula is a molecular formula, false otherwise.
 */
declare function isMolecularFormula(formula: Formula): formula is MolecularFormula;

declare function isProofItemInferred(x: ProofItem): x is ProofItemInferred;

declare function isPropositionalVariable(formula: Formula | string): formula is PropositionalVariable;

declare function eliminateDoubleNegations(formula: Formula): Formula;

declare function buildConjunctionString(premises: string[]): string;

declare function haveEvenNumberOfNegations(formula: Formula): boolean;

declare function parseToFormulaObject(formula: string): Formula;
declare function parseToFormulaString(formula: Formula): string;

declare function printTruthTable(truthTable: TruthTable): void;

declare function implication(left: Formula, right: Formula): Implication;
declare function biconditional(left: Formula, right: Formula): Biconditional;
declare function conjunction(left: Formula, right: Formula): Conjunction;
declare function disjunction(left: Formula, right: Formula): Disjunction;
declare function negation(value: Formula): Negation;

declare class InvalidFormulaException extends Error {
}

declare class InferenceException extends Error {
}

declare class InvalidProofSequenceException extends Error {
}

declare class UnrecognizedTokenException extends Error {
}

/**
 * A class that provides methods to build formulas with
 * the artificial language of logic syntax.
 */
declare class Builder {
    private static operations;
    private static biconditional;
    private static conjunction;
    private static disjunction;
    private static implication;
    private static buildRecursively;
    /**
     * Builds a formula with the syntax of logic.
     * @param formula - The logical formula to build.
     * @returns The builded logical formula.
     * @throws {InvalidFormulaException}
     */
    static buildFormula(formula: Formula): string;
}

/**
 * Parser class for analyzing tokens and creating a logical formula tree.
 */
declare class Parser {
    tokens: Token[];
    private token;
    private lastIsVariable;
    /**
     * Constructor of the Parser class.
     * @param tokens Array of tokens to be analyzed.
     */
    constructor(tokens: Token[]);
    /**
     * Performs the analysis of the tokens and returns the logical formula tree.
     * @returns The logical formula resulting from the analysis of the tokens.
     */
    parse(): Formula;
    private process;
    private next;
    private node;
    private isUnary;
}

/**
 * Class responsible for defining the inference rules.
 */
declare class RuleSetter {
    protected static BiconditionalIntroduction(conditional1: Implication, conditional2: Implication): Biconditional;
    protected static BiconditionalElimination(biconditional: Biconditional): Conjunction;
    protected static ConditionalProof(hypothesis: Formula, conclusionOfHypothesis: Formula): Implication;
    protected static Conditionalization(formula: Formula, conditional: Implication): Implication;
    protected static Commutativity(formula: Conjunction | Disjunction | Biconditional): Conjunction | Disjunction | Biconditional;
    protected static Contraposition(formula: Implication): Formula;
    protected static ConjunctionIntroduction(formula1: Formula, formula2: Formula): Conjunction;
    protected static ConjunctionElimination(conjunction: Conjunction): [Formula, Formula];
    protected static DeMorgan(formula: Negation | Disjunction | Conjunction): Negation | Conjunction | Disjunction;
    protected static DisjunctionIntroduction(formula: Formula, disjunction: Disjunction): Disjunction;
    protected static DisjunctiveSyllogism(disjunction: Disjunction, negatedDisjunct: Negation): Formula;
    protected static ImplicationElimination(conditional: Implication): Disjunction;
    protected static ImplicationNegation(negation: Negation): Conjunction;
    protected static DoubleNegation(formula: Formula): Formula;
    protected static DoubleNegationIntroduction(formula: Formula): Negation;
    protected static ConjunctionOverDisjunctionDistribution(formula: Conjunction): {
        operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
        left: {
            operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
            left: Formula;
            right: Formula;
        };
        right: {
            operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
            left: Formula;
            right: Formula;
        };
    };
    protected static DisjunctionOverConjunctionDistribution(formula: Disjunction): {
        operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
        left: {
            operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
            left: Formula;
            right: Formula;
        };
        right: {
            operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
            left: Formula;
            right: Formula;
        };
    };
    protected static ConjunctionAssociativity(formula: Conjunction): Conjunction;
    protected static DisjunctionAssociativity(formula: Disjunction): Disjunction;
    protected static BiconditionalAssociativity(formula: Biconditional): Biconditional;
    protected static HypotheticalSyllogism(conditional1: Implication, conditional2: Implication): Formula;
    protected static ModusPonens(conditional: Implication, antecedent: Formula): Formula;
    protected static ModusTollens(conditional: Implication, negatedConsequent: Negation): Formula;
    protected static ReductioAdAbsurdum(conditional: Implication): Negation;
    private static DistributeRecursively;
    private static Distribute;
    private static Associate;
}

/**
 * Class responsible for, through a test and its items, applying the inference rules defined by the RuleSetter class.
 */
declare class RuleApplier extends RuleSetter {
    static biconditionalIntroduction(item: ProofItemInferred, proof: Proof): Biconditional;
    static biconditionalElimination(item: ProofItemInferred, proof: Proof): Conjunction;
    static conditionalization(item: ProofItemInferred, proof: Proof): Implication;
    static conjunctionIntroduction(item: ProofItemInferred, proof: Proof): Conjunction;
    static conjunctionElimination(item: ProofItemInferred, proof: Proof): [Formula, Formula];
    static commutativity(item: ProofItemInferred, proof: Proof): Conjunction | Disjunction | Biconditional;
    static contraposition(item: ProofItemInferred, proof: Proof): Formula;
    static deMorgan(item: ProofItemInferred, proof: Proof): Negation | Conjunction | Disjunction;
    static disjunctionIntroduction(item: ProofItemInferred, proof: Proof): Disjunction;
    static disjunctiveSyllogism(item: ProofItemInferred, proof: Proof): Formula;
    static doubleNegation(item: ProofItemInferred, proof: Proof): Formula;
    static doubleNegationIntroduction(item: ProofItemInferred, proof: Proof): Negation;
    static hypotheticalSyllogism(item: ProofItemInferred, proof: Proof): Formula;
    static implicationElimination(item: ProofItemInferred, proof: Proof): Disjunction;
    static implicationNegation(item: ProofItemInferred, proof: Proof): Conjunction;
    static modusPonens(item: ProofItemInferred, proof: Proof): Formula;
    static modusTollens(item: ProofItemInferred, proof: Proof): Formula;
    static conjunctionOverDisjunctionDistribution(item: ProofItemInferred, proof: Proof): {
        operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
        left: {
            operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
            left: Formula;
            right: Formula;
        };
        right: {
            operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
            left: Formula;
            right: Formula;
        };
    };
    static disjunctionOverConjunctionDistribution(item: ProofItemInferred, proof: Proof): {
        operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
        left: {
            operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
            left: Formula;
            right: Formula;
        };
        right: {
            operation: "Biconditional" | "Conjunction" | "Disjunction" | "Implication";
            left: Formula;
            right: Formula;
        };
    };
    static conjunctionAssociativity(item: ProofItemInferred, proof: Proof): Conjunction;
    static disjunctionAssociativity(item: ProofItemInferred, proof: Proof): Disjunction;
    static biconditionalAssociativity(item: ProofItemInferred, proof: Proof): Biconditional;
    static conditionalProof(item: ProofItemInferred, proof: Proof): Implication;
    static reductioAdAbsurdum(item: ProofItemInferred, proof: Proof): Negation;
    private static throwsIfIsNotEqual;
    private static throwsIfLengthDoesntMatch;
    private static throwsIfIndexDoesntExist;
}

/**
 * Lexer class for tokenizing propositional logic formulas.
 */
declare class Lexer {
    input: string;
    private tokens;
    private pointer;
    private c;
    private operator;
    /**
     * Creates a new Lexer instance.
     * @param formula The propositional logic formula to tokenize.
     */
    constructor(formula: string);
    /**
     * Tokenizes the propositional logic formula.
     * @returns An array of tokens representing the formula.
     */
    lex(): Token[];
    private next;
    private push;
    private isWhiteSpace;
    private isVariable;
    private isSpecial;
    private isExpressionBoundary;
    private operatorExists;
    private throwTokenException;
}

/**
 * A class that provides methods to reduce formulas, which use implication or biconditional, to use only negations, conjunctions and disjunctions.
 */
declare class Reducer {
    /**
     * Recursively reduces a logical formula to its reduced form based on its operation.
     * @param x - The logical formula to reduce.
     * @returns The reduced logical formula.
     */
    private static reduceFormula;
    /**
     * Reduces a Biconditional to a Conjunction.
     * @param x - The Biconditional operation to reduce.
     * @returns The reduced Conjunction formula.
     */
    static biconditional(x: Biconditional): Conjunction;
    /**
     * Reduces an Implication to a Disjunction
     * @param x - The formula to reduce.
     * @returns The reduced Disjunction formula.
     */
    static implication(x: Implication): Disjunction;
    /**
     * Reduces both sides of a Conjunction
     * @param x - The formula to reduce.
     * @returns The reduced Conjunction formula.
     */
    static conjunction(x: Conjunction): Conjunction;
    /**
     * Reduces both sides of a Disjunction
     * @param x - The formula to reduce.
     * @returns The reduced Disjunction formula.
     */
    static disjunction(x: Disjunction): Disjunction;
    /**
     * Reduces the negated formula
     * @param x - The formula to reduce.
     * @returns The reduced Negation formula.
     */
    static negation(x: Negation): Negation;
}

declare const frege: Frege;

export { AtomicFormula, Biconditional, BinaryOperation, BinaryOperationFormula, Boundary, Builder, Calculator, Conjunction, Disjunction, Formula, Frege, INFERENCE_RULES, Implication, InferenceException, InferenceRule, InvalidFormulaException, InvalidProofSequenceException, Lexer, MappedProof, MolecularFormula, Negation, Operator, Parser, Proof, ProofChecker, ProofEndOfHypothesis, ProofItem, ProofItemBase, ProofItemInferred, ProofItemType, PropositionalVariable, PropositionalVariableValues, Reducer, RuleApplier, RuleSetter, Token, TokenMap, TokenType, TruthTable, TruthValue, UnaryOperation, UnrecognizedTokenException, biconditional, buildConjunctionString, conjunction, disjunction, eliminateDoubleNegations, frege, haveEvenNumberOfNegations, implication, inferenceRulesMap, isArrayString, isBiconditional, isBinaryOperationFormula, isConjunction, isContradiction, isDisjunction, isEndOfHypothesis, isHypothesis, isImplication, isMolecularFormula, isNegation, isProofItemInferred, isPropositionalVariable, negation, parseToFormulaObject, parseToFormulaString, printTruthTable };