# #include "paramod.h"

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

## Contents

- Public Routines
- Public Definitions
- Introduction

## Public Routines in File paramod.c

#### Index

| para_from_into | para_pos | paramodulate
basic_paramodulation_prunes | para_instance_prunes | para_pos2 |

#### Details

    void paramodulation_options(BOOL ordered_inference,
    			    BOOL check_instances,
    			    BOOL positive_inference,
    			    BOOL basic_paramodulation,
    			    BOOL para_from_vars,
    			    BOOL para_into_vars,
    			    BOOL para_from_small);

    int basic_paramodulation_prunes(void);

How many paramodulants were killed because they failed the "basic" test.

    void para_from_into(Topform from, Context cf,
    		    Topform into, Context ci,
    		    BOOL check_top,
    		    void (*proc_proc) (Topform));

Paramodulate from one clause into another (non-backtrack unification version).

For oriented equality atoms, we go from left sides only and into both sides. For nonoriented equality atoms, we go from and into both sides.

    int para_instance_prunes();

    Topform para_pos(Topform from_clause, Ilist from_pos,
    		 Topform into_clause, Ilist into_pos);

Construct a paramodulant from the given data. A fatal error occurs if it does not exist. In building the justification, the position vectors are copied.

    Topform para_pos2(Topform from, Ilist from_pos, Topform into, Ilist into_pos);

Construct a paramodulant from the given data. A fatal error occurs if it does not exist. In building the justification, the position vectors are copied. This is similar to para_pos(), except that it allows the into_term to be a variable.

    Topform paramodulate(Literals from_lit, int from_side, Context from_subst,
    		     Topform into_clause, Ilist into_pos, Context into_subst);

## Public Definitions in File paramod.h

    /* where to paramodulate into */

    typedef enum { PARA_ALL,
    	       PARA_ALL_EXCEPT_TOP,
    	       PARA_TOP_ONLY } Para_loc;

## Introduction

This package has a paramodulation inference rule.