Automated Reasoning

DOI10.1007/B98691zbMath1126.68578OpenAlexW4239036627MaRDI QIDQ5307061

Stephan Schulz

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

Mathematics Subject Classification ID

Related Items (18)

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

This page was built for publication: Automated Reasoning