Import 19/10/2011Obsahem diplomové práce je vytvoření e-learningového systému, který studenty interaktivně vyučuje problematice obecné rezoluční metody a ověřuje také jejich znalosti. Systém kontroluje každý krok studenta a na základě požadavku je schopen i napovídat, jaký další krok má student udělat. Mimo vytvořený systém tato diplomová práce obsahuje také souhrn teorie predikátové logiky prvního řádu (PL1) související s touto problematikou a souhrn syntaktických důkazových metod v predikátové logice prvního řádu.Content of this diploma thesis includes the description of newly generated e-learning system, which interactively teaches students how to use general resolution method and also checks their knowledges. System checks each student´...