Automated Reasoning
From MaRDI portal
Publication:5307061
DOI10.1007/b98691zbMath1126.68578OpenAlexW4239036627MaRDI QIDQ5307061
Publication date: 25 September 2007
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b98691
Related Items
Automatic Proof and Disproof in Isabelle/HOL ⋮ First-order logic formalisation of impossibility theorems in preference aggregation ⋮ Encoding Monomorphic and Polymorphic Types ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Consequence-based and fixed-parameter tractable reasoning in description logics ⋮ Translating higher-order clauses to first-order clauses ⋮ Simple and Efficient Clause Subsumption with Feature Vector Indexing ⋮ On the independence of axioms in BL and MTL ⋮ Perfect Discrimination Graphs: Indexing Terms with Integer Exponents ⋮ From LCF to Isabelle/HOL ⋮ Extending Sledgehammer with SMT Solvers ⋮ Experimenting with Deduction Modulo ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ On Transfinite Knuth-Bendix Orders ⋮ Lightweight relevance filtering for machine-generated resolution problems ⋮ Computing finite models by reduction to function-free clause logic ⋮ E Theorem Prover ⋮ Extending Sledgehammer with SMT solvers
