E_AXFILTER(1)

📦
version 3.5.1 · 8 versions
, in ubuntu stonking

💖 E_AXFILTER(1) 💖

okay so bestie, welcome to the manual for e_axfilter 💅 it lives in the User Commands part of the manual, and it's here to do one very specific lil job for you. let's get into it 🫶

✨ NAME ✨

e_axfilter — the manual page for e_axfilter 3.5.1 Countess Grey 👑

🌸 SYNOPSIS 🌸

e_axfilter [options] [files]

🦋 DESCRIPTION 🦋

e_axfilter 3.5.1 "Countess Grey" 💜

So what does this actually do? This program applies SinE-like goal-directed filters to a problem specification (which is, like, a set of clauses and/or formulas) to generate reduced problem specifications. Those are way easier for a theorem prover to handle, but they're still likely to contain all the axioms necessary for a proof — if one exists, that is. no cap 🧚

In default mode, the program reads a problem specification and an (optional) filter specification, and produces one reduced output file for each filter given. ✨

Not me about to drop the important bit: while all standard input formats are supported (LOP, TPTP-2 and TPTP-3), output is only and automatically in TPTP-3. 🎀

Also highkey different from the rest of the crew: unlike most of the other tools in the E distribution, this program does not support pipe-based input and output, since it uses file names generated from the input file name and filter names to store the different result files. so don't pipe it, bestie, it will simply not vibe 😭

💅 OPTIONS 💅

  • -h, --help — print a short description of program usage and options. the little "what am i even doing" moment 🙈
  • -V, --version — print the version number of the prover. please include this with all bug reports (if any). 👑
  • -v, --verbose[=<arg>] — verbose comments on the progress of the program. this technical information is printed to stderr. the short form, or the long form without the optional argument, is equivalent to --verbose=1. 📢
  • -o <arg>, --output-file=<arg> — redirect output into the named file (this affects only some output, as most is written to automatically generated files based on the input and filter names). 🗂️
  • -s, --silent — equivalent to --output-level=0. shhh, silence is golden 🤫
  • -l <arg>, --output-level=<arg> — select an output level; greater values imply more verbose output. 📈
  • -f <arg>, --filter=<arg> — specify the filter definition file. if not set, the system will uses the built-in default. 🎀
  • -S, --seed-symbols[=<arg>] — enable artificial seeding of the axiom selection process and determine which symbol classes should be used to generate different sets. the argument is a string of letters, each indicating one class of symbols to use: 'p' indicates predicate symbols, 'f' non-constant function symbols, and 'c' constants. note that this will create potentially multiple output files for each activated symbols. 🌱 the short form, or the long form without the optional argument, is equivalent to --seed-symbols=p.
  • --seeds=<arg> — explicitly specify the symbols that should be used as seed symbols for axiom extraction. this overwrites --seed-subsample and --seed-symbols. 💥
  • --seed-subsample[=<arg>] — subsample from the set of eligible seed symbols. the argument is a one-character designator for the method ('m' uses the symbols that occur in the most input formulas, 'l' uses the symbols that occur in the least number of formulas, and 'r' samples randomly), followed by the number of symbols to select. the option without the optional argument is equivalent to --seed-subsample=r1000. 🎲
  • -m, --seed-method[=<arg>] — specify how to select seed axioms when artificial seeding is used. the argument is a string of letters, each indicating one method to use. the letters are: 'l': use the syntactically largest axiom in which the seed symbol occurs. 'd': use the most diverse axiom in which the seed symbol occurs, i.e. the symbol with the largest set of different symbols. 'a': use all axioms in which the seed symbol occurs. for 'l' and 'd', if there are multiple candidates, use the first one. if the option is not set, 'a' is assumed. 🧠 the short form, or the long form without the optional argument, is equivalent to --seed-method=lda.
  • -d, --dump-filter — print the filter definition in force. dump it, bestie 🗑️✨
  • --lop-in — set E-LOP as the input format. if no input format is selected by this or one of the following options, E will guess the input format based on the first token. it will almost always correctly recognize TPTP-3, but it may misidentify E-LOP files that use TPTP meta-identifiers as logical symbols. 🤔
  • --lop-format — equivalent to --lop-in.
  • --tptp-in — parse TPTP-2 format instead of E-LOP (but note that includes are handled according to TPTP-3 semantics). 🎀
  • --tptp-format — equivalent to --tptp-in.
  • --tptp2-in — synonymous with --tptp-in.
  • --tptp2-format — synonymous with --tptp-in.
  • --tstp-in — parse TPTP-3 format instead of E-LOP (note that TPTP-3 syntax is still under development, and the version in E may not be fully conforming at all times. E works on all TPTP 6.3.0 FOF and CNF input files (including includes). 🚧
  • --tstp-format — equivalent to --tstp-in.
  • --tptp3-in — synonymous with --tstp-in.
  • --tptp3-format — synonymous with --tstp-in.

🐛 REPORTING BUGS 🐛

Report bugs to <schulz@eprover.org>. please include the following, if possible: 🥺

  • The version of the package as reported by eprover --version.
  • The operating system and version.
  • The exact command line that leads to the unexpected behaviour.
  • A description of what you expected and what actually happened.
  • If possible all input files necessary to reproduce the bug.

Copyright 1998-2026 by Stephan Schulz, schulz@eprover.org, and the E contributors (see DOC/CONTRIBUTORS).

This program is a part of the distribution of the equational theorem prover E. you can find the latest version of the E distribution as well as additional information at http://www.eprover.org 🌈

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. see the GNU General Public License for more details. ⚠️ (fr fr, no warranty, don't come for her)

You should have received a copy of the GNU General Public License along with this program (it should be contained in the top level directory of the distribution in the file COPYING); if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

We welcome bug reports and even reasonable questions. if the prover behaves in an unexpected way, please include the following information: 💌

  • What did you observe? - What did you expect? - The output of eprover --version - The full commandline that lead to the unexpected behaviour - The input file(s) that lead to the unexpected behaviour

Most bug reports should be send to <schulz@eprover.org>. bug reports with respect to the HO-version should be send to or at least copied to <jasmin.blanchette@gmail.com>. please remember that this is an unpaid volunteer service. 🙏

The original copyright holder can be contacted via email or as

Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik
Lerchenstrasse 1 70174 Stuttgart Germany

aaaand that's the whole thing bestie, you ate it 💅✨ this was e_axfilter 3.5.1 Countess Grey, from August 2026, and it lives in the E_AXFILTER(1) page of the manual. go filter some axioms, you icon 🎀🦋💖

📦 where this page comes from