1.  13
    A Framework for the Transfer of Proofs, Lemmas and Strategies From Classical to Non Classical Logics.Ricardo Caferra, Stéphane Demri & Michel Herment - 1993 - Studia Logica 52 (2):197 - 232.
    There exist valuable methods for theorem proving in non classical logics based on translation from these logics into first-order classical logic (abbreviated henceforth FOL). The key notion in these approaches istranslation from aSource Logic (henceforth abbreviated SL) to aTarget Logic (henceforth abbreviated TL). These methods are concerned with the problem offinding a proof in TL by translating a formula in SL, but they do not address the very important problem ofpresenting proofs in SL via a backward translation. We propose a (...)
    Direct download (5 more)  
    Export citation  
  2.  8
    Review of Witold Marciszewski and Roman Murawski: Mechanization of Reasoning in a Historical Perspective. [REVIEW]Ricardo Caferra - 1996 - Journal of Applied Non-Classical Logics 6 (3):287-288.
  3.  7
    A Term-Graph Clausal Logic: Completeness and Incompleteness Results★.Ricardo Caferra, Rachid Echahed & Nicolas Peltier - 2008 - Journal of Applied Non-Classical Logics 18 (4):373-411.
    A clausal logic allowing to handle term-graphs is defined. Term-graphs are a generalization of terms possibly containing shared subterms and cycles. The satisfiability problem for this logic is shown to be undecidable, but some fragments are identified for which it is semi-decidable. A complete calculus for these fragments is proposed. Some simple examples give a taste of this calculus at work.
    Direct download (3 more)  
    Export citation