A Focused Sequent Calculus for Higher-Order Logic

DOI10.1007/978-3-319-08587-6_5zbMATH Open1423.68421OpenAlexW29796863MaRDI QIDQ3192181FDOQ3192181

Fredrik Lindblad

Publication date: 26 September 2014

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08587-6_5

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03)

Cited In (13)

• A sequent calculus for first-order logic formalized in Isabelle/HOL
• Solving modal logic problems by translation to higher-order logic
• Superposition with lambdas
• Title not available (Why is that?)
• Extensional higher-order paramodulation in Leo-III
• Focused and Synthetic Nested Sequents
• Title not available (Why is that?)
• A logical calculus for problem solving in highly structured application domains
• Superposition with lambdas
• A combinator-based superposition calculus for higher-order logic
• GRUNGE: a grand unified ATP challenge
• A coding method for a sequent calculus of propositional logic
• Title not available (Why is that?)

Uses Software

• TPTP
• Curry
• Agda
• AgsyHOL

   Recommendations

• Sequent calculus for hybrid logic 👍 👎
• A sequent calculus for first-order logic formalized in Isabelle/HOL 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• A sequent calculus and a theorem prover for standard conditional logics 👍 👎
• Labelled sequent calculus for inquisitive logic 👍 👎
• A formal framework for specifying sequent calculus proof systems 👍 👎
• Sequent calculi for choice logics 👍 👎
• Title not available (Why is that?) 👍 👎

This page was built for publication: A Focused Sequent Calculus for Higher-Order Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192181)