Computation with run time skolemisation (N-Prolog part 3)

DOI10.1080/11663081.1993.10510797zbMath0798.68031OpenAlexW2000240460MaRDI QIDQ4275698

Uwe Reyle, Dov M. Gabbay

Publication date: 1 February 1994

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/11663081.1993.10510797

zbMATH Keywords

unificationintuitionistic logicSkolem functionsPrologclassical logictheorem proveralgorithmic proof systemhuman oriented theorem provinglogic of Skolem functionstime stamping

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17)

Related Items (3)

Direct deductive computation on discourse representation structures ⋮ A family of goal directed theorem provers based on conjunction and implication. I ⋮ Correspondences between classical, intuitionistic and uniform provability

Cites Work

• A family of goal directed theorem provers based on conjunction and implication. I
• N-Prolog: An extension of Prolog with hypothetical implications. I.
• N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure
• Direct deductive computation on discourse representation structures

This page was built for publication: Computation with run time skolemisation (N-Prolog part 3)