/* $Id: FormulaChecker.java,v 1.3 2005/06/08 21:55:56 m31 Exp $ * * This file is part of the project "Hilbert II" - http://www.qedeq.org * * Copyright 2000-2005, Michael Meyling . * * "Hilbert II" is free software; you can redistribute * it and/or modify it under the terms of the GNU General Public * License as published by the Free Software Foundation; either * version 2 of the License, or (at your option) any later version. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. */ package org.qedeq.kernel.bo.logic; import org.qedeq.kernel.base.elli.Element; import org.qedeq.kernel.base.elli.ElementList; import org.qedeq.kernel.dto.elli.ElementSet; /** * This class deals with {@link org.qedeq.kernel.base.elli.Element}s which represent a * formula. It has methods to check those elements for certain criteria. * * @version $Revision: 1.3 $ * @author Michael Meyling */ public final class FormulaChecker { /** Operator string for logical "and". */ public static final String CONJUNCTION_OPERATOR = "AND"; /** Operator string for logical "or". */ public static final String DISJUNCTION_OPERATOR = "OR"; /** Operator string for logical implication. */ public static final String IMPLICATION_OPERATOR = "IMPL"; /** Operator string for logical equivalence. */ public static final String EQUIVALENCE_OPERATOR = "EQUI"; /** Operator string for logical negation. */ public static final String NEGATION_OPERATOR = "NOT"; /** Operator string for predicate constants. */ public static final String PREDICATE_OPERATOR = "PRED"; /** Operator string for subject variables. */ public static final String SUBJECT_VARIABLE_OPERATOR = "VAR"; /** Operator string for proposition variables. */ public static final String PROPOSITION_VARIABLE_OPERATOR = "PROP"; /** Operator string for predicate variables. */ public static final String PREDICATE_VARIABLE_OPERATOR = "PREDVAR"; /** Operator string for predicate argument list. */ public static final String LIST_OPERATOR = "L"; /** Operator string for logical "all" operator. */ public static final String UNIVERSAL_QUANTIFIER_OPERATOR = "FORALL"; /** Operator string for logical "exists" operator. */ public static final String EXISTENTIAL_QUANTIFIER_OPERATOR = "EXISTS"; /** Error message: first argument must be an atom. */ private static final String FIRST_ARGUMENT_MUST_BE_AN_ATOM = "first argument must be an atom"; /** Error message: second argument must be a list. */ private static final String SECOND_ARGUMENT_MUST_BE_A_LIST = "second argument must be a list"; /** * Constructor. */ private FormulaChecker() { // nothing to do } /** * Is {@link Element} a formula? * * @param element check this element * @throws CheckException if it is no formula */ public static final void checkFormula(final Element element) throws CheckException { if (element.isAtom()) { throw new CheckException("an atom is no formula", element); } final ElementList list = element.getList(); final String operator = list.getOperator(); if (operator.equals(CONJUNCTION_OPERATOR) || operator.equals(DISJUNCTION_OPERATOR) || operator.equals(IMPLICATION_OPERATOR) || operator.equals(EQUIVALENCE_OPERATOR)) { if (list.size() <= 1) { throw new CheckException( "more than one argument expected", element); } // check if all arguments are formulas and no bound variables // are free and vice versa final ElementSet free = new ElementSet(); final ElementSet bound = new ElementSet(); for (int i = 0; i < list.size(); i++) { FormulaChecker.checkFormula(list.getElement(i)); final ElementSet newFree = FormulaChecker.getFreeSubjectVariables(list.getElement(i)); final ElementSet newBound = FormulaChecker.getBoundSubjectVariables(list.getElement(i)); if (!newFree.newIntersection(bound).isEmpty()) { throw new CheckException( "these free variables are already bound in previous formulas: " + newFree, list.getElement(i)); } if (!newBound.newIntersection(free).isEmpty()) { throw new CheckException( "these bound variables are already free in previous formulas: " + newBound, list.getElement(i)); } bound.union(newBound); free.union(newFree); } } else if (operator.equals(NEGATION_OPERATOR)) { if (list.size() != 1) { throw new CheckException( "negation requires exactly one argument", element); } FormulaChecker.checkFormula(list.getElement(0)); } else if (operator.equals(PROPOSITION_VARIABLE_OPERATOR)) { // check if there is exactly one numeric argument if (list.size() != 1) { throw new CheckException("exactly one numeric argument expected", element); } // check if first argument is an atom if (!list.getElement(0).isAtom()) { throw new CheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM, element); } } else if (operator.equals(PREDICATE_VARIABLE_OPERATOR)) { if (list.size() != 2) { throw new CheckException("exactly two arguments expected", element); } // check if first argument is an atom if (!list.getElement(0).isAtom()) { throw new CheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM, element); } // check if second argument is list of subject variables if (!list.getElement(1).isList()) { throw new CheckException(SECOND_ARGUMENT_MUST_BE_A_LIST, element); } final ElementList vars = list.getElement(1).getList(); if (!vars.getOperator().equals(LIST_OPERATOR)) { throw new CheckException("list operator expected", vars); } for (int i = 0; i < list.size(); i++) { FormulaChecker.checkSubjectVariable(list.getElement(i)); } } else if (list.getOperator().equals(EXISTENTIAL_QUANTIFIER_OPERATOR) || list.getOperator().equals(UNIVERSAL_QUANTIFIER_OPERATOR)) { if (list.size() != 2) { throw new CheckException("exactly two arguments expected", element); } // check if first argument is subject variable FormulaChecker.checkSubjectVariable(list.getElement(0)); // check if second argument is a formula FormulaChecker.checkFormula(list.getElement(1)); // check if subject variable is free in formula if (!FormulaChecker.getFreeSubjectVariables(list.getElement(1)).contains( list.getElement(0))) { throw new CheckException("subject variable not free in formula", list.getElement(0)); } } else { throw new CheckException("not a logical operator", element); } } /** * Is {@link Element} an subject variable? * * @param element check this element * @return is is an atomic element */ public static final boolean isSubjectVariable(final Element element) { try { FormulaChecker.checkSubjectVariable(element); } catch (CheckException e) { return false; } return true; } /** * Is {@link Element} an subject variable? * * @param element check this element * @throws CheckException if it is no subject variable */ public static final void checkSubjectVariable(final Element element) throws CheckException { if (!element.isList() && element.getList().getOperator().equals(SUBJECT_VARIABLE_OPERATOR) && element.getList().size() == 1) { // check if first argument is an atom if (!element.getList().getElement(0).isAtom()) { throw new CheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM, element); } } else { throw new CheckException("subject variable expected", element); } } /** * Return all free subject variables of an element. * * @param element check this element * @return all free subject variables */ public static final ElementSet getFreeSubjectVariables(final Element element) { final ElementSet free = new ElementSet(); if (FormulaChecker.isSubjectVariable(element)) { free.add(element); } else if (element.isList()) { final ElementList list = element.getList(); final String operator = list.getOperator(); if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR) || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) { for (int i = 1; i < list.size(); i++) { free.union(FormulaChecker.getFreeSubjectVariables(list.getElement(i))); } free.remove(list.getElement(0)); } else { for (int i = 0; i < list.size(); i++) { free.union(FormulaChecker.getFreeSubjectVariables(list.getElement(i))); } } } return free; } /** * Return all bound subject variables of an element. * * @param element check this element * @return all bound subject variables */ public static final ElementSet getBoundSubjectVariables(final Element element) { final ElementSet bound = new ElementSet(); if (element.isList()) { ElementList list = element.getList(); final String operator = list.getOperator(); if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR) || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) { for (int i = 1; i < list.size(); i++) { bound.union(FormulaChecker.getBoundSubjectVariables( list.getElement(i))); } bound.add(list.getElement(0)); } else { for (int i = 0; i < list.size(); i++) { bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i))); } } } return bound; } }