 |
Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
|
|
Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
|
| Cadd_current_clause | Collection of more complex semantic actions |
| Cadd_fof_formula | More complex semantic action for FOF formulas |
| Cschedule::add_step | Semantic action for parser |
| Cschedule::add_time | Semantic action for parser |
| CClause | Representation of clauses |
| CClauseCopyCache | |
| CClauseLengthCompare | Provide a function object to compare clauses by size |
| Cclear_current_clause | Collection of more complex semantic actions |
| Ctptp_parser::cnf_annotated_struct | Parser's representation of a Clause |
| Cansi_escape_colours::Colour | |
| Ccolour_string::ColourString | Simple addition of colour to strings and ostreams |
| Ccommas::comma | Simple function object for putting commas in lists |
| CCommentStatus | One of several basic semantic actions |
| Ccursor_symbols::Cursor | Simple library for doing things involving moving the curser when producing terminal output |
| CDefinedAdder | One of several basic semantic actions |
| CDistinctAdder | One of several basic semantic actions |
| ▼Cstd::exception | |
| Cfile_open_exception | Exception used by the application in main(...) |
| Cfile_parse_exception | Exception used by the application in main(...) |
| Cfile_read_exception | Exception used by the application in main(...) |
| CFileIncludeAdder | One of several basic semantic actions |
| CFOF | Representation of first order formulas |
| Ctptp_parser::fof_plain_term_struct | Recursive data structure for Terms |
| Cfun_hash | Hashing for functions using the Boost library for hashing |
| CFunction | Basic representation of functions |
| CFunctionIndex | Mechanism for looking after functions |
| ▼Cqi::grammar | |
| Cschedule::schedule_grammar< It > | |
| Ctptp_parser::TPTP_file_grammar< It > | |
| Ctptp_parser::cnf_annotated_grammar< It > | |
| Ctptp_parser::cnf_formula_grammar< It > | |
| Ctptp_parser::fof_annotated_grammar< It > | |
| Ctptp_parser::fof_atomic_formula_grammar< It > | |
| Ctptp_parser::fof_defined_infix_formula_grammar< It > | |
| Ctptp_parser::fof_formula_grammar< It > | |
| Ctptp_parser::fof_infix_unary_grammar< It > | |
| Ctptp_parser::fof_term_grammar< It > | |
| Ctptp_parser::include_grammar< It > | |
| Ctptp_parser::literal_grammar< It > | |
| CInferenceItem | Full representation of inferences, beyond just the name |
| Ctptp_parser::infix_struct | Structure for fof_defined_infix_formula and fof_infix_unary |
| CInterval | Simple class to help you count intervals |
| CLemmata | Representation of the lemma list |
| CLiteral | Basic representation of literals, bundling together (pointers to) a Predicate, a collection of arguments each a (pointer to a) Term, an arity and a polarity |
| Cunicode_symbols::LogSym | |
| Cmake_fof_formula | More complex semantic action for FOF formulas |
| CMatrix | Representation of the Matrix within a proof |
| Cschedule::next_settings | Semantic action for parser |
| Cparams | Structure containing all the command line and other options |
| CPredicate | Basic representation of predicates: here just names, ids and arities |
| CPredicateIndex | Management of Predicate objects |
| Cprint_cnf_formula_name | Semantic action for cnf_formula |
| Cprint_cnf_formula_role | Semantic action for cnf_formula |
| Cprint_fof_formula_name | Semantic action for fof_formula |
| Cprint_fof_formula_role | Semantic action for fof_formula |
| CProofChecker | |
| CProofPrinter | Class for rendering a proof in various formats |
| Cschedule::Schedule | Wrap up the parsing process and the operation of a schedule in a single class |
| Cset_neg_lit | Collection of more complex semantic actions |
| Cschedule::set_step | Semantic action for parser |
| Cschedule::set_value | Semantic action for parser |
| Cshow_fof_formula | Display FOL formulas as you parse |
| Cshow_lit | Collection of more complex semantic actions |
| CSimplePath | Simple representation of the path within a proof tree |
| CStack | If you implement the stacks used by the prover as a vector<StackItem> then every time you move down the stack a StackItem destructor is called. This ends up eating about 1/6th of the runtime, and is completely unnecessary |
| CStackItem | Stack items: each contains its own material for generating possible next inferences |
| CStackProver | Prover using a pair of stacks to conduct the proof search |
| ▼Cboost::static_visitor | |
| Cconvert_fof_arguments_struct | More complex semantic actions, now functions etc to make a literal |
| Cconvert_fof_atomic_formula | More complex semantic actions, now functions etc to make a literal |
| Cconvert_fof_formula | More complex semantic action for FOF formulas |
| Cshow_fof_formula_type | You have to make fof_plain_term_struct etc something that boost::fusion can use |
| CSubstitution | General representation of a substitution |
| CSubstitutionStack | As you build a proof you make substitutions that apply to the entire proof: if you backtrack during the search you need to remove the relevant substitutions |
| CSystemAdder | One of several basic semantic actions |
| CTerm | General representation of terms |
| Cterm_hash | Hashing for terms using the Boost library |
| CTermIndex | Look after terms, using hash consing to avoid storing copies of terms |
| Cto_lit | Collection of more complex semantic actions |
| CTPTPParser | Wrap up everything the TPTP parser needs to do inside a single class |
| CUnifier | Wrap up various applications of unificiation into a single class: all the unification you need to do happens here |
| Cunset_neg_lit | Collection of more complex semantic actions |
| CVariable | Basic representation of variables |
| CVariableIndex | Storage of named variables, and management of new, anonymous and unique variables |
| Cverbose_print::VPrint |
1.12.0