Cited in
(only showing first 100 items - show all)- Inductive theorem proving based on tree grammars
- scientific article; zbMATH DE number 1303351 (Why is no real title available?)
- Large theory reasoning with SUMO at CASC
- Race against the teens -- benchmarking mechanized math on pre-university problems
- Integrating simplex with tableaux
- Relaxed weighted path order in theorem proving
- Automatic acquisition of search control knowledge from multiple proof attempts.
- Efficient model generation through compilation.
- Blocked clauses in first-order logic
- scientific article; zbMATH DE number 1809864 (Why is no real title available?)
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Blocking and other enhancements for bottom-up model generation methods
- Old or heavy? Decaying gracefully with age/weight shapes
- Restricted combinatory unification
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- Nagging: A distributed, adversarial search-pruning technique applied to first-order inference
- Herbrand constructivization for automated intuitionistic theorem proving
- Algorithmic introduction of quantified cuts
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Faster, higher, stronger: E 2.3
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Conjecture synthesis for inductive theories
- Heaps and Data Structures: A Challenge for Automated Provers
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- First-order atom definitions extended
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Bayesian ranking for strategy scheduling in automated theorem provers
- Lash 1.0 (system description)
- SCL(EQ): SCL for first-order logic with equality
- Vampire getting noisy: Will random bits help conquer chaos? (system description)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- JEFL: joint embedding of formal proof libraries
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- AC simplifications and closure redundancies in the superposition calculus
- GKC: a reasoning system for large knowledge bases
- Logic for Programming, Artificial Intelligence, and Reasoning
- Logic for Programming, Artificial Intelligence, and Reasoning
- Embedding and automating conditional logics in classical higher-order logic
- Superposition with lambdas
- A scalable module system
- Connection tableau calculi with disjunctive constraints
- Understanding Resolution Proofs through Herbrand’s Theorem
- Advances in Artificial Intelligence – SBIA 2004
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
- The CADE-26 automated theorem proving system competition -- CASC-26
- Scavenger 0.1: a theorem prover based on conflict resolution
- Machine learning for first-order theorem proving
- Model elimination without contrapositives
- An interactive derivation viewer
- Building proofs or counterexamples by analogy in a resolution framework
- Evolving combinators
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Automated theorem proving in quasigroup and loop theory
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- The TM system for repairing non-theorems
- scientific article; zbMATH DE number 1301750 (Why is no real title available?)
- scientific article; zbMATH DE number 1882060 (Why is no real title available?)
- Fast term indexing with coded context trees
- Presenting and explaining Mizar
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- (Dual) hoops have unique halving
- scientific article; zbMATH DE number 1222430 (Why is no real title available?)
- scientific article; zbMATH DE number 1389651 (Why is no real title available?)
- On the generation of quantified lemmas
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- On using ground joinable equations in equational theorem proving
- Eliminating redundant search space on backtracking for forward chaining theorem proving
- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
- Mathematical applications of inductive logic programming
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- Satallax: An Automatic Higher-Order Prover
- Towards Verifying Logic Programs in the Input Language of clingo
- First order Stålmarck. Universal lemmas through branch merges
- Efficient instance retrieval with standard and relational path indexing
- scientific article; zbMATH DE number 1980938 (Why is no real title available?)
- scientific article; zbMATH DE number 2043541 (Why is no real title available?)
- scientific article; zbMATH DE number 1487985 (Why is no real title available?)
- EUCLID
- Management of Change in Declarative Languages
- Dependently Typed Programming Based on Automated Theorem Proving
- The TPTP problem library
- Cut-elimination for quantified conditional logic
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- HOL Based First-Order Modal Logic Provers
- A set solver for finite set relation algebra
- Extensional higher-order paramodulation in Leo-III
- The Relative Power of Semantics and Unification
- Computing Tiny Clause Normal Forms
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
- TPTP, TSTP, CASC, etc.
- Formal logic definitions for interchange languages
- A domain-independent system for modeling number theory using first-order predicate logic
- Incremental variable splitting
- scientific article; zbMATH DE number 5872266 (Why is no real title available?)
- MPTP 0.1 -- system description
- Verifying Tight Logic Programs with anthem and vampire
- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
- Using the TPTP Language for Writing Derivations and Finite Interpretations
This page was built for software: TPTP
