Switch to: References

Add citations

You must login to add citations.
  1. On the formalization of semantic conventions.James G. Williams - 1990 - Journal of Symbolic Logic 55 (1):220-243.
    This paper discusses six formalization techniques, of varying strengths, for extending a formal system based on traditional mathematical logic. The purpose of these formalization techniques is to simulate the introduction of new syntactic constructs, along with associated semantics for them. We show that certain techniques (among the six) subsume others. To illustrate sharpness, we also consider a selection of constructs and show which techniques can and cannot be used to introduce them. The six studied techniques were selected on the basis (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  • Induction and Skolemization in saturation theorem proving.Stefan Hetzl & Jannik Vierling - 2023 - Annals of Pure and Applied Logic 174 (1):103167.
  • Steps Toward a Computational Metaphysics.Branden Fitelson & Edward N. Zalta - 2007 - Journal of Philosophical Logic 36 (2):227-247.
    In this paper, the authors describe their initial investigations in computational metaphysics. Our method is to implement axiomatic metaphysics in an automated reasoning system. In this paper, we describe what we have discovered when the theory of abstract objects is implemented in PROVER9 (a first-order automated reasoning system which is the successor to OTTER). After reviewing the second-order, axiomatic theory of abstract objects, we show (1) how to represent a fragment of that theory in PROVER9's first-order syntax, and (2) how (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  • Proof normalization modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
    We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • ALONZO: Deduktionsagenten höherer Ordnung für Mathematische Assistenzsysteme.Benzmüller Christoph - 2003
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark