[Svinja]

Вообще, программа перднацначена для доказательства сиквенций, путем построения семантических деревьев доказательств.

структура: к корню присоединено поле, в котором создаются мувики формул, каждый мувик формулы, хранит в себе отображение самой формулы(A&B->C,C|-A->B) и древовидную структуру этой формулы(для удобства автопроверок истинности). Для этого я создавал классы для каждой булевой функции(and,or,not, и тд) например класс конъюнкции:

class TKonjunction extends Object
{
  public var leftPart:Number;
  public var rightPart:Number;
	
  public function True(AA:Boolean,AB:Boolean,AC:Boolean,AD:Boolean,AE:Boolean,AF:Boolean):Boolean
  {
    return _root['pole']['sc'+_root['pole']['currSc']]['formula'+this['leftPart']].True(AA,AB,AC,AD,AE,AF) && _root['pole']['sc'+_root['pole']['currSc']]['formula'+this['rightPart']].True(AA,AB,AC,AD,AE,AF);
  }
	
  public function Show():String
  {
    return _root['pole']['sc'+_root['pole']['currSc']]['formula'+this['leftPart']].Show() + '&' + _root['pole']['sc'+_root['pole']['currSc']]['formula'+this['rightPart']].Show();
  }
}

Здесь два поля: левая часть конъюнкции и правая, но там хранятся номера элементов(!), а не указатели. И два рекурсивных метода(правда даже позороно называть их методами) проверки истенности(на вход подаем значения 6-ти переменных) и записи формулы в виде строки. Если б были указатели, то код измнеился бы так:

class TKonjunction extends TFormula
{
  public var leftPart:*TFormula;
  public var rightPart:*TFormula;
	
  public function True(AA:Boolean,AB:Boolean,AC:Boolean,AD:Boolean,AE:Boolean,AF:Boolean):Boolean
  {
    return this['leftPart']->True(AA,AB,AC,AD,AE,AF) && this['rightPart']->True(AA,AB,AC,AD,AE,AF);
  }
	
  public function Show():String
  {
    return this['leftPart']->Show() + '&' + this['rightPart']->Show();
  }
}