| |
| |
| Mathematical theory exploration | |
| |
| |
| |
| Searching while keeping a trace : the evolution from satisfiability to knowledge compilation | |
| |
| |
| |
| Representing and reasoning with operational semantics | |
| |
| |
| |
| Flyspeck I : tame graphs | |
| |
| |
| |
| Automatic construction and verification of isotopy invariants | |
| |
| |
| |
| Pitfalls of a full floating-point proof : example on the formal proof of the Veltkamp/Dekker algorithms | |
| |
| |
| |
| Using the TPTP language for writing derivations and finite interpretations | |
| |
| |
| |
| Stratified context unification is NP-complete | |
| |
| |
| |
| A logical characterization of forward and backward chaining in the inverse method | |
| |
| |
| |
| Connection tableaux with lazy paramodulation | |
| |
| |
| |
| Blocking and other enhancements for bottom-up model generation methods | |
| |
| |
| |
| The MathServe system for semantic Web reasoning services | |
| |
| |
| |
| System description : GCLCprover + GeoThms | |
| |
| |
| |
| A sufficient completeness checker for linear order-sorted specifications Modulo Axioms | |
| |
| |
| |
| Extending the TPTP language to higher-order logic with automated parser generation | |
| |
| |
| |
| Extracting programs from constructive HOL proofs via IZF set-theoretic semantics | |
| |
| |
| |
| Towards self-verification of HOL light | |
| |
| |
| |
| An interpretation of Isabelle/HOL in HOL light | |
| |
| |
| |
| Combining type theory and untyped set theory | |
| |
| |
| |
| Cut-simulation in impredicative logics | |
| |
| |
| |
| Interpolation in local theory extensions | |
| |
| |
| |
| Canonical Gentzcn-type Calculi with (n,k)-ary quantifiers | |
| |
| |
| |
| Dynamic logic with non-rigid functions | |
| |
| |
| |
| AProVE 1.2 : automatic termination proofs in the dependency pair framework | |
| |
| |
| |
| CEL - a polynomial-time reasoner for life science ontologies | |
| |
| |
| |
| FaCT++ description logic reasoner : system description | |
| |
| |
| |
| Importing HOL into Isabelle/HOL | |
| |
| |
| |
| Geometric resolution : a proof procedure based on finite model search | |
| |
| |
| |
| A powerful technique to eliminate isomorphism in finite model search | |
| |
| |
| |
| Automation of recursive path ordering for infinite labelled rewrite systems | |
| |
| |
| |
| Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic | |
| |
| |
| |
| Eliminating redundancy in higher-order unification : a lightweight approach | |
| |
| |
| |
| First-order logic with dependent types | |
| |
| |
| |
| Automating proofs in category theory | |
| |
| |
| |
| Formal global optimisation with taylor models | |
| |
| |
| |
| A purely functional library for modular arithmetic and its application to certifying large prime numbers | |
| |
| |
| |
| Proving formally the implementation of an efficient gcd algorithm for polynomials | |
| |
| |
| |
| A SAT-based decision procedure for the subclass of unrollable list formulas in ACL2 (SULFA) | |
| |
| |
| |
| Solving sparse linear constraints | |
| |
| |
| |
| Inferring network invariants automatically | |
| |
| |
| |
| A recursion combinator for nominal datatypes implemented in Isabelle/HOL | |
| |
| |
| |
| Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures | |
| |
| |
| |
| Verifying mixed real-integer quantifier elimination | |
| |
| |
| |
| Presburger modal logic is PSPACE-complete | |
| |
| |
| |
| Tree automata with equality constraints modulo equational theories | |
| |
| |
| |
| CASC-J3 - the 3rd IJCAR ATP system competition | |
| |
| |
| |
| Matrix interpretations for proving termination of term rewriting | |
| |
| |
| |
| Partial recursive functions in higher-order logic | |
| |
| |
| |
| On the strength of proof-irrelevant type theories | |
| |
| |
| |
| Consistency and completeness of rewriting in the calculus of constructions | |
| |
| |
| |
| Specifying and reasoning about dynamic access-control policies | |
| |
| |
| |
| On keys and functional dependencies as first-class citizens in description logics | |
| |
| |
| |
| A resolution-based decision procedure for SHOIQ | |
| |