First-order unification in the PVS proof assistant

, , &
Logic Journal of the IGPL 22 (5):758-789 (2014)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1093/jigpal/jzu012

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,202

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

On the complexity of Bounded Second-Order Unification and Stratified Context Unification.Jordi Levy, Manfred Schmidt-schauß & Mateu Villaret - 2011 - Logic Journal of the IGPL 19 (6):763-789.
Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions.Flávio L. C. de Moura, Mauricio Ayala-Rincón & Fairouz Kamareddine - 2008 - Journal of Applied Logic 6 (1):72-108.
The undecidability of the second order predicate unification problem.Gilles Amiot - 1990 - Archive for Mathematical Logic 30 (3):193-199.
A Syntactic Approach to Unification in Transitive Reflexive Modal Logics.Rosalie Iemhoff - 2016 - Notre Dame Journal of Formal Logic 57 (2):233-247.
A unification-theoretic method for investigating the k-provability problem.William M. Farmer - 1991 - Annals of Pure and Applied Logic 51 (3):173-214.
Newton’s notion and practice of unification.Steffen Ducheyne - 2005 - Studies in History and Philosophy of Science Part A 36 (1):61-78.
Isabelle/Hol a Proof Assistant for Higher-Order Logic.Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel - 2002 - Berlin and New York: Springer.
Intuitionistic completeness of first-order logic.Robert Constable & Mark Bickford - 2014 - Annals of Pure and Applied Logic 165 (1):164-198.
Unification via the λse-style of explicit substitutions.M. Ayala-rincón & F. Kamareddine - 2001 - Logic Journal of the IGPL 9 (4):489-523.
Unification neural networks: unification by error-correction learning.Ekaterina Komendantskaya - 2011 - Logic Journal of the IGPL 19 (6):821-847.
On me number of steps in proofs.Jan Krajíèek - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.
On the number of steps in proofs.Jan Kraj\mIček - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.
Comparing and implementing calculi of explicit substitutions with eta-reduction.Mauricio Ayala-Rincón, Flávio L. C. de Moura & Fairouz Kamareddine - 2005 - Annals of Pure and Applied Logic 134 (1):5-41.
Higher-order automated theorem proving.Michael Kohlhase - unknown
Notes on a formalization of the prime number theorem.Jeremy Avigad - unknown

Analytics

Added to PP
2016-06-30

Downloads
19 (#750,145)

6 months
3 (#880,460)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Mariana Rincon
University of São Paulo

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references