A Combinator-Based Superposition Calculus for Higher-Order Logic

We present a refutationally complete superposition calculus for a version of higher-order logic based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other lea...

Descripción completa

Detalles Bibliográficos
Autores principales: Bhayat, Ahmed, Reger, Giles
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324226/
http://dx.doi.org/10.1007/978-3-030-51074-9_16
_version_ 1783551896540151808
author Bhayat, Ahmed
Reger, Giles
author_facet Bhayat, Ahmed
Reger, Giles
author_sort Bhayat, Ahmed
collection PubMed
description We present a refutationally complete superposition calculus for a version of higher-order logic based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other leading higher-order provers. The results suggest that the method is competitive.
format Online
Article
Text
id pubmed-7324226
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73242262020-06-30 A Combinator-Based Superposition Calculus for Higher-Order Logic Bhayat, Ahmed Reger, Giles Automated Reasoning Article We present a refutationally complete superposition calculus for a version of higher-order logic based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other leading higher-order provers. The results suggest that the method is competitive. 2020-05-30 /pmc/articles/PMC7324226/ http://dx.doi.org/10.1007/978-3-030-51074-9_16 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Bhayat, Ahmed
Reger, Giles
A Combinator-Based Superposition Calculus for Higher-Order Logic
title A Combinator-Based Superposition Calculus for Higher-Order Logic
title_full A Combinator-Based Superposition Calculus for Higher-Order Logic
title_fullStr A Combinator-Based Superposition Calculus for Higher-Order Logic
title_full_unstemmed A Combinator-Based Superposition Calculus for Higher-Order Logic
title_short A Combinator-Based Superposition Calculus for Higher-Order Logic
title_sort combinator-based superposition calculus for higher-order logic
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324226/
http://dx.doi.org/10.1007/978-3-030-51074-9_16
work_keys_str_mv AT bhayatahmed acombinatorbasedsuperpositioncalculusforhigherorderlogic
AT regergiles acombinatorbasedsuperpositioncalculusforhigherorderlogic
AT bhayatahmed combinatorbasedsuperpositioncalculusforhigherorderlogic
AT regergiles combinatorbasedsuperpositioncalculusforhigherorderlogic

Ejemplares similares