dfs_interpretation.pl -- Model-theoretic interpretation

Model-theoretic interpretation.

 dfs_variables(-Variables) is det

Variables is a list of variables.

 dfs_entities(+N, -Entities) is det

Entities is a list of N model entities.

 dfs_constant_instantiations(+Model, -ConstantInstantiations) is det

ConstantInstantiations is a list of all constant instantiations in Model.

 dfs_term_instantiations(+Model, +G, -TermInstantiations) is det

TermInstantiations is a list of all constant and variable instantiations in Model.

 dfs_init_g(+Model, -G) is det

Initializes the assignment function G :: Var -> Um. Variables are assigned by iterating over the entities in the Model universe.

 dfs_assign(+G, +Model, +Assignments, -Gprime) is det

Updates the assignment function G of Model with variable Assignments, yielding assignment function G'.

 dfs_terms_to_entities(?Terms, +TermInstantiations, ?Entities) is det

Maps Terms into Entities (or vice versa), given their instantiations.

 dfs_formula_to_fol(+Formula, -FOLFormula) is det

Convert FOL and/or DRS formula into first-order logic formula.

 dfs_formulas_to_fol(+Formulas, -FOLFormulas) is det

Convert FOL and/or DRS formulas into first-order logic formulas.

 dfs_interpret(+Formula, +Model) is semidet

dfs_interpret(+FormulaSet, +Model) is semidet

Evaluates the truth value of Formula in Model, given an initial assignment function G.

 dfs_interpret(+Formula, +Model, +G) is semidet

dfs_interpret(+FormulaSet, +Model, +G) is semidet

Evaluates the truth value of Formula in Model, given the assignment function G.