![]() |
Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
|
| ▼Nansi_escape_colours | |
| CColour | |
| ▼Ncolour_string | |
| CColourString | Simple addition of colour to strings and ostreams |
| ▼Ncommas | |
| Ccomma | Simple function object for putting commas in lists |
| ▼Ncursor_symbols | |
| CCursor | Simple library for doing things involving moving the curser when producing terminal output |
| ▼Nschedule | Hide all the global stuff in this namespace |
| Cadd_step | Semantic action for parser |
| Cadd_time | Semantic action for parser |
| Cnext_settings | Semantic action for parser |
| CSchedule | Wrap up the parsing process and the operation of a schedule in a single class |
| Cschedule_grammar | |
| Cset_step | Semantic action for parser |
| Cset_value | Semantic action for parser |
| ▼Ntptp_parser | The tptp_parser namespace contains a lot of stuff that's essentially just global |
| Ccnf_annotated_grammar | |
| Ccnf_annotated_struct | Parser's representation of a Clause |
| Ccnf_formula_grammar | |
| Cfof_annotated_grammar | |
| Cfof_atomic_formula_grammar | |
| Cfof_defined_infix_formula_grammar | |
| Cfof_formula_grammar | |
| Cfof_infix_unary_grammar | |
| Cfof_plain_term_struct | Recursive data structure for Terms |
| Cfof_term_grammar | |
| Cinclude_grammar | |
| Cinfix_struct | Structure for fof_defined_infix_formula and fof_infix_unary |
| Cliteral_grammar | |
| CTPTP_file_grammar | |
| ▼Nunicode_symbols | Vic_string - "verbose/indented/coloured" |
| CLogSym | |
| ▼Nverbose_print | |
| CVPrint | |
| Cadd_current_clause | Collection of more complex semantic actions |
| Cadd_fof_formula | More complex semantic action for FOF formulas |
| CClause | Representation of clauses |
| CClauseCopyCache | |
| CClauseLengthCompare | Provide a function object to compare clauses by size |
| Cclear_current_clause | Collection of more complex semantic actions |
| CCommentStatus | One of several basic semantic actions |
| 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 |
| CDefinedAdder | One of several basic semantic actions |
| CDistinctAdder | One of several basic semantic actions |
| CERWA | Implementation of the ERWA algorithm for multiarmed bandits |
| CEXP3 | Implementation of the EXP3 algorithm for multiarmed bandits |
| 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 |
| Cfun_hash | Hashing for functions using the Boost library for hashing |
| CFunction | Basic representation of functions |
| CFunctionIndex | Mechanism for looking after functions |
| CInferenceItem | Full representation of inferences, beyond just the name |
| 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 |
| Cmake_fof_formula | More complex semantic action for FOF formulas |
| CMatrix | Representation of the Matrix within a proof |
| 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 |
| Cset_neg_lit | Collection of more complex semantic actions |
| Cshow_fof_formula | Display FOL formulas as you parse |
| Cshow_fof_formula_type | You have to make fof_plain_term_struct etc something that boost::fusion can use |
| Cshow_lit | Collection of more complex semantic actions |
| CSimplePath | Simple representation of the path within a proof tree |
| 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 |
| 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 |
| CUCB | Implementation of the UCB algorithm for multiarmed bandits |
| 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 |