A Focused Sequent Calculus for Higher-Order Logic

DOI10.1007/978-3-319-08587-6_5MaRDI QIDQ3192181zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Sequent calculus for hybrid logic
• A sequent calculus for first-order logic formalized in Isabelle/HOL
• A first-order sequent calculus for logical inferentialists and expressivists
• scientific article; zbMATH DE number 218517
• scientific article; zbMATH DE number 1223614
• 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
• A multi-succedent sequent calculus for logical expressivists

Cited in

(15)

• A sequent calculus for first-order logic formalized in Isabelle/HOL
• Extensional higher-order paramodulation in Leo-III
• A coding method for a sequent calculus of propositional logic
• scientific article; zbMATH DE number 1795222 (Why is no real title available?)
• scientific article; zbMATH DE number 7561320 (Why is no real title available?)
• Focused and Synthetic Nested Sequents
• Theorem Proving in Higher Order Logics
• Analytic tableaux for higher-order logic with choice
• scientific article; zbMATH DE number 7350767 (Why is no real title available?)
• Superposition with lambdas
• A combinator-based superposition calculus for higher-order logic
• A logical calculus for problem solving in highly structured application domains
• Solving modal logic problems by translation to higher-order logic
• Superposition with lambdas
• GRUNGE: a grand unified ATP challenge

Describes a project that uses

Uses Software

• TPTP
• Curry
• Agda
• AgsyHOL

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)