Two Versions of MGTP:
Ground MGTP
(MGTP/G)		 Non-Ground MGTP
(MTGP/N)
Problem Non-Horn and ground Horn and non-ground
Application E.g. Database problems E.g. Mathematical theorems
Programming
Techniques
  • Direct use of KL1 variables
  • Translation given clauses
    to KL1 clauses
  • Efficient coding
    using head unification of
    KL1
  • Representing variables
    with ground terms
  • Interpreting a given set of
    clauses
  • Using "meta-library"
    E.g. Unification with occur
    check
Parallelization AND/OR parallel AND parallel


Key Technologies to improve Efficiency:
Problem Technology
Redundancy in
Conjunctive Matching		 RAMS(RamifiedStack)
MERC(Multi-Entry Repeated Combination)
Irrelevant Clauses Partial falsify relevancy test
Over Generation
of Models		 Lazy model generation
Parallelism OR parallelization for non-Horn problems
AND parallelization(Model distributing/
sharing) for Horn problems
Unification/
Subsumption		 Clause compiling technique
Term indexing memory


					- 65 -