#include "basic.h"

This page has information from files basic.h and basic.c.

Public Routines in File basic.c

Term apply_basic(Term t, Context c);

This is similar to apply(), but it makes "nonbasic" marks for "basic paramodulation".

Term apply_basic_substitute(Term t, Term beta, Context c_from,
			    Term into_term, Context c_into);

This is similar to apply_substitute(), but it makes "nonbasic" marks for "basic paramodulation".

BOOL basic_paramod(void);

Is basic paramodulation enabled?

BOOL basic_term(Term t);

Check if a term is basic. This simply checks the "nonbasic" mark.

void clear_all_nonbasic_marks(Term t);

void init_basic_paramod(void);

void mark_all_nonbasic(Term t);

void mark_term_nonbasic(Term t);

int nonbasic_flag(void);

BOOL nonbasic_term(Term t);

Check if a term is nonbasic. This simply checks the "nonbasic" mark.

void p_term_basic(Term t);

void set_basic_paramod(BOOL flag);

Set or clear basic paramodulation.