← Back to branch summary

~ubuntu-branches/ubuntu/saucy/ladr/saucy

« back to all changes in this revision

Viewing changes to ladr/parautil.h.bak

  • Committer: Package Import Robot
  • Author(s): Frank Lichtenheld
  • Date: 2013-05-25 11:43:32 UTC
  • mfrom: (5.1.5 sid)
  • Revision ID: package-import@ubuntu.com-20130525114332-lkzco1dti2hwrf7v
Tags: 0.0.200911a-2
* QA upload.
* Upload to unstable.
* Change maintainer to QA group.

Show diffs side-by-side

added added

removed removed

Lines of Context:
ladr/parautil.h.bak
1
 
/*  Copyright (C) 2006, 2007 William McCune
2
 
 
3
 
    This file is part of the LADR Deduction Library.
4
 
 
5
 
    The LADR Deduction Library is free software; you can redistribute it
6
 
    and/or modify it under the terms of the GNU General Public License,
7
 
    version 2.
8
 
 
9
 
    The LADR Deduction Library is distributed in the hope that it will be
10
 
    useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
11
 
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
 
    GNU General Public License for more details.
13
 
 
14
 
    You should have received a copy of the GNU General Public License
15
 
    along with the LADR Deduction Library; if not, write to the Free Software
16
 
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
17
 
*/
18
 
 
19
 
#ifndef TP_PARAUTIL_H
20
 
#define TP_PARAUTIL_H
21
 
 
22
 
 #include "just.h"
23
 
 
24
 
/* INTRODUCTION
25
 
This package contains a few utilites for paramodulation and demodulation.
26
 
*/
27
 
 
28
 
/* Public definitions */
29
 
 
30
 
/* End of public definitions */
31
 
 
32
 
/* Public function prototypes from parautil.c */
33
 
 
34
 
void init_paramod(void);
35
 
 
36
 
void mark_renamable_flip(Term atom);
37
 
 
38
 
BOOL renamable_flip_eq(Term atom);
39
 
 
40
 
BOOL renamable_flip_eq_test(Term atom);
41
 
 
42
 
void mark_oriented_eq(Term atom);
43
 
 
44
 
BOOL oriented_eq(Term atom);
45
 
 
46
 
BOOL same_term_structure(Term t1, Term t2);
47
 
 
48
 
void flip_eq(Term atom, int n);
49
 
 
50
 
void orient_equalities(Topform c, BOOL allow_flips);
51
 
 
52
 
BOOL eq_tautology(Topform c);
53
 
 
54
 
Term top_flip(Term a);
55
 
 
56
 
void zap_top_flip(Term a);
57
 
 
58
 
Literals literal_flip(Literals a);
59
 
 
60
 
void zap_literal_flip(Literals a);
61
 
 
62
 
Topform new_constant(Topform c, int new_sn);
63
 
 
64
 
Topform fold_denial(Topform c, int alpha_max);
65
 
 
66
 
BOOL equational_def_2(Term alpha, Term beta);
67
 
 
68
 
int equational_def(Topform c);
69
 
 
70
 
Ordertype unfold_order(Term alpha, Term beta);
71
 
 
72
 
Topform build_reflex_eq(void);
73
 
 
74
 
#endif  /* conditional compilation of whole file */