Extensional higher-order paramodulation in Leo-III
From MaRDI portal
Publication:2666959
DOI10.1007/s10817-021-09588-xOpenAlexW3148132267MaRDI QIDQ2666959
Alexander Steen, Christoph Benzmüller
Publication date: 23 November 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1907.11501
equational reasoninghigher-order logicextensionalityautomated theorem provingquantified modal logicsnonclassical logicsHenkin semanticsLeo-III
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (5)
SAT-Inspired Higher-Order Eliminations ⋮ Making higher-order superposition work ⋮ Local is best: efficient reductions to modal logic \textsf{K} ⋮ Lash 1.0 (system description) ⋮ Local reductions for the modal cube
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The higher-order prover \textsc{Leo}-II
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- Combining and automating classical and non-classical logics in classical higher-order logics
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- TPS: A hybrid automatic-interactive system for developing proofs
- Computer supported mathematics with \(\Omega\)MEGA
- Computer science -- theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3--7, 2007. Proceedings
- Lightweight relevance filtering for machine-generated resolution problems
- The undecidability of the second-order unification problem
- Isabelle/HOL. A proof assistant for higher-order logic
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Superposition for \(\lambda\)-free higher-order logic
- The higher-order prover Leo-III
- Higher-order unification revisited: Complete sets of transformations
- An introduction to mathematical logic and type theory: To truth through proof.
- Alpha-conversion and typability
- Quantified multimodal logics in simple type theory
- Extending SMT solvers to higher-order logic
- Restricted combinatory unification
- GRUNGE: a grand unified ATP challenge
- Extending Sledgehammer with SMT solvers
- Cut-elimination for quantified conditional logic
- Translating higher-order clauses to first-order clauses
- Effective Normalization Techniques for HOL
- Automating Free Logic in Isabelle/HOL
- Agent-Based HOL Reasoning
- HOL Based First-Order Modal Logic Provers
- The TPTP Typed First-Order Form with Arithmetic
- Satallax: An Automatic Higher-Order Prover
- The QMLTP Problem Library for First-Order Modal Logics
- Encoding Monomorphic and Polymorphic Types
- Multimodal and intuitionistic logics in simple type theory
- HOL Light: An Overview
- A Focused Sequent Calculus for Higher-Order Logic
- MleanCoP: A Connection Prover for First-Order Modal Logic
- Intensional models for the theory of types
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- A Brief Overview of HOL4
- Handling Polymorphism in Automated Deduction
- Cut-Simulation and Impredicativity
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- A Linear Spine Calculus
- Theorem Provers For Every Normal Modal Logic
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Explicit substitutions
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Higher-order semantics and extensionality
- Resolution in type theory
- The undecidability of unification in third order logic
- General models, descriptions, and choice in type theory
- General models and extensionality
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Completeness in the theory of types
- A Functional calculus of first order based on strict implication
- Superposition with lambdas
- The MET: The Art of Flexible Reasoning with Modalities
This page was built for publication: Extensional higher-order paramodulation in Leo-III
