OTTER

swMATH2904MaRDI QIDQ15442FDOQ15442

Author name not available (Why is that?)

Described by source

• Automatic theorem proving and OTTER

Cited In (only showing first 100 items - show all)

• Building Theorem Provers
• Automated reasoning with power maps
• The application of automated reasoning to formal models of combinatorial optimization
• Heaps and Data Structures: A Challenge for Automated Provers
• Old or heavy? Decaying gracefully with age/weight shapes
• A note on assumptions about Skolem functions
• A posthumous contribution by Larry Wos: excerpts from an unpublished column
• A Wos Challenge Met
• Larry Wos: visions of automated reasoning
• Set of support, demodulation, paramodulation: a historical perspective
• An efficient subsumption test pipeline for BS(LRA) clauses
• Retrieving geometric information from images: the case of hand-drawn diagrams
• On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
• History and Prospects for First-Order Automated Deduction
• When is the commutant of a Bol loop a subloop?
• Title not available (Why is that?)
• Three-variable statements of set-pairing
• Learning to solve geometric construction problems from images
• MACE4 and SEM: A Comparison of Finite Model Generators
• OTTER experiments in a system of combinatory logic
• A generic graphic framework for combining inference tools and editing proofs and formulae
• Computational Verification of Network Programs in Coq
• A comprehensive framework for saturation theorem proving
• Making higher-order superposition work
• Missing proofs found
• Title not available (Why is that?)
• Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach
• Learning theorem proving components
• OTTER Proofs in Tarskian Geometry
• Substitution tree indexing
• Extending E Prover with Similarity Based Clause Selection Strategies
• Implementing Euclid's straightedge and compass constructions in type theory
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• First Order Logic with Domain Conditions
• The Legacy of a Great Researcher
• Partial matching for analogy discovery in proofs and counter-examples
• Implementing Superposition in iProver (System Description)
• Limited second-order functionality in a first-order setting
• Title not available (Why is that?)
• Extended path-indexing
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Mechanizing Mathematical Reasoning
• Layered map reasoning
• Title not available (Why is that?)
• Distributivity in Ł\(_{\aleph_0}\) and other sentential logics
• Title not available (Why is that?)
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Presenting inequations in mathematical proofs
• : A Resolution-Based Prover for Multimodal K
• Goals and benchmarks for automated map reasoning
• System Description: E.T. 0.1
• A model and a first analysis of distributed-search contraction-based strategies
• An algorithm for the retrieval of unifiers from discrimination trees
• Subgoal strategies for solving board puzzles
• Automated Deduction in Ring Theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the desirability of mechanizing calculational proofs
• Automatic derivation of the irrationality of \(e\)
• Towards the qualitative, plan-based simulation of international crises
• Mathematical applications of inductive logic programming
• Computer proofs about finite and regular sets: The unifying concept of subvariance.
• Title not available (Why is that?)
• Foundations of Information and Knowledge Systems
• Principal rings and their invariant factors
• The hot list strategy
• Shortest axiomatizations of implicational S4 and S5
• On the notion of interestingness in automated mathematical discovery
• OTTER and the Moufang identity problem
• Title not available (Why is that?)
• AI*IA 2005: Advances in Artificial Intelligence
• The kernel strategy and its use for the study of combinatory logic
• Computing answers with model elimination
• Exploiting functional dependencies in declarative problem specifications
• Automated proofs of equality problems in Overbeek's competition
• The problem of induction
• Uniform strategies: The CADE-11 theorem proving contest
• On subsumption in distributed derivations
• Problem solving by searching for models with a theorem prover
• Meeting the challenge of fifty years of logic
• The linked inference principle. I: The formal treatment
• Finite differences/elements in classical beam problems: Derivation of feasibility conditions under parametric inequality constraints with the help of Reduce and REDLOG
• Semantic trees revisited: Some new completeness results
• Automated reasoning about cubic curves
• Single identities for ternary Boolean algebras
• Commutativity Theorems in Groups with Power-like Maps
• Title not available (Why is that?)
• Efficient model generation through compilation
• A semantic backward chaining proof system
• A learning procedure for mathematics.
• The application of automated reasoning to questions in mathematics and logic
• Towards automating duality
• Ordered tableaux: Extensions and applications
• Integration of automated and interactive theorem proving in ILF
• The power of combining resonance with heat
• Title not available (Why is that?)

This page was built for software: OTTER