diff --git a/web/authors/steen/index.html b/web/authors/steen/index.html new file mode 100644 --- /dev/null +++ b/web/authors/steen/index.html @@ -0,0 +1,96 @@ + + + + + + Alexander Steen- Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Alexander Steen

+
+ + + +
+
+ + +

Entries

2022

+ + + + +
+
+ + + \ No newline at end of file diff --git a/web/authors/steen/index.xml b/web/authors/steen/index.xml new file mode 100644 --- /dev/null +++ b/web/authors/steen/index.xml @@ -0,0 +1,20 @@ + + + + steen on Archive of Formal Proofs + /authors/steen/ + Recent content in steen on Archive of Formal Proofs + Hugo -- gohugo.io + en-gb + Mon, 05 Dec 2022 00:00:00 +0000 + + Automation of Boolos' Curious Inference in Isabelle/HOL + /entries/Boolos_Curious_Inference_Automated.html + Mon, 05 Dec 2022 00:00:00 +0000 + + /entries/Boolos_Curious_Inference_Automated.html + + + + + diff --git a/web/authors/sutcliffe/index.html b/web/authors/sutcliffe/index.html new file mode 100644 --- /dev/null +++ b/web/authors/sutcliffe/index.html @@ -0,0 +1,96 @@ + + + + + + Geoff Sutcliffe- Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Geoff Sutcliffe

+
+ + + +
+
+ + +

Entries

2022

+ + + + +
+
+ + + \ No newline at end of file diff --git a/web/authors/sutcliffe/index.xml b/web/authors/sutcliffe/index.xml new file mode 100644 --- /dev/null +++ b/web/authors/sutcliffe/index.xml @@ -0,0 +1,20 @@ + + + + sutcliffe on Archive of Formal Proofs + /authors/sutcliffe/ + Recent content in sutcliffe on Archive of Formal Proofs + Hugo -- gohugo.io + en-gb + Mon, 05 Dec 2022 00:00:00 +0000 + + Automation of Boolos' Curious Inference in Isabelle/HOL + /entries/Boolos_Curious_Inference_Automated.html + Mon, 05 Dec 2022 00:00:00 +0000 + + /entries/Boolos_Curious_Inference_Automated.html + + + + + diff --git a/web/entries/Boolos_Curious_Inference_Automated.html b/web/entries/Boolos_Curious_Inference_Automated.html new file mode 100644 --- /dev/null +++ b/web/entries/Boolos_Curious_Inference_Automated.html @@ -0,0 +1,159 @@ + + + + + + Automation of Boolos' Curious Inference in Isabelle/HOL - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Automation of Boolos' Curious Inference in Isabelle/HOL

+
+ +

Christoph Benzmüller 📧, David Fuenmayor 📧, Alexander Steen and Geoff Sutcliffe +

+ + +

December 5, 2022

+ +
+

Abstract

+ +
Boolos’ Curious Inference is automated in Isabelle/HOL after interactive speculation of a suitable shorthand notation (one or two definitions).
+ +

License

+
BSD License

Topics

+

Related publications

+
  • + Benzmüller, C., Fuenmayor, D., Steen, A., & Sutcliffe, G. (2022). Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers. ArXiv. https://doi.org/10.48550/ARXIV.2208.06879 +
+

Session Boolos_Curious_Inference_Automated

+
+ + +
+
+ + + +
+ +
+

Cite

+ × +
+ 
@article{Boolos_Curious_Inference_Automated-AFP,
+  author  = {Christoph Benzmüller and David Fuenmayor and Alexander Steen and Geoff Sutcliffe},
+  title   = {Automation of Boolos' Curious Inference in Isabelle/HOL},
+  journal = {Archive of Formal Proofs},
+  month   = {December},
+  year    = {2022},
+  note    = {\url{https://isa-afp.org/entries/Boolos_Curious_Inference_Automated.html},
+            Formal proof development},
+  ISSN    = {2150-914x},
+}
+ Download +
+
+
+ +
+ +
+

Download

+ × + Download latest + +
+
+
+
+ + + \ No newline at end of file diff --git a/web/theories/boolos_curious_inference_automated/index.html b/web/theories/boolos_curious_inference_automated/index.html new file mode 100644 --- /dev/null +++ b/web/theories/boolos_curious_inference_automated/index.html @@ -0,0 +1,83 @@ + + + + + + Boolos_Curious_Inference_Automated - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Boolos_Curious_Inference_Automated

+
+ + +
+
+

Boolos_Curious_Inference_Automated

+
+
+ + + \ No newline at end of file diff --git a/web/topics/logic/index.html b/web/topics/logic/index.html new file mode 100644 --- /dev/null +++ b/web/topics/logic/index.html @@ -0,0 +1,959 @@ + + + + + + Logic - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Logic

+
+ + +
+

Subject Classification

ACM: Theory of computation~Logic

AMS: Mathematical logic and foundations

2023

+ + + +

2022

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +

2021

+ + + + + + + + + + + + + +

2020

+ + + + + + + + + + + + + + + + + + +

2019

+ + + + + + + + + +

2018

+ + + + + + + + + +

2017

+ + + + + + + + + + + +

2016

+ + + + + + + + + + + + + + +

2015

+ + + +

2014

+ + + + + +

2013

+ + + + + + +

2011

+ + +

2010

+ + + +

2009

+ + + + +

2008

+ + + +

2007

+ + +

2005

+ + +

2004

+ + + + + +
+
+ + + \ No newline at end of file diff --git a/web/topics/logic/index.xml b/web/topics/logic/index.xml new file mode 100644 --- /dev/null +++ b/web/topics/logic/index.xml @@ -0,0 +1,1091 @@ + + + + Logic on Archive of Formal Proofs + /topics/logic/ + Recent content in Logic on Archive of Formal Proofs + Hugo -- gohugo.io + en-gb + Mon, 09 Jan 2023 00:00:00 +0000 + + Synthetic Completeness + /entries/Synthetic_Completeness.html + Mon, 09 Jan 2023 00:00:00 +0000 + + /entries/Synthetic_Completeness.html + + + + + Synthetic Completeness + /entries/Synthetic_Completeness.html + Mon, 09 Jan 2023 00:00:00 +0000 + + /entries/Synthetic_Completeness.html + + + + + Automation of Boolos' Curious Inference in Isabelle/HOL + /entries/Boolos_Curious_Inference_Automated.html + Mon, 05 Dec 2022 00:00:00 +0000 + + /entries/Boolos_Curious_Inference_Automated.html + + + + + Automation of Boolos' Curious Inference in Isabelle/HOL + /entries/Boolos_Curious_Inference_Automated.html + Mon, 05 Dec 2022 00:00:00 +0000 + + /entries/Boolos_Curious_Inference_Automated.html + + + + + Automation of Boolos' Curious Inference in Isabelle/HOL + /entries/Boolos_Curious_Inference_Automated.html + Mon, 05 Dec 2022 00:00:00 +0000 + + /entries/Boolos_Curious_Inference_Automated.html + + + + + Automation of Boolos' Curious Inference in Isabelle/HOL + /entries/Boolos_Curious_Inference_Automated.html + Mon, 05 Dec 2022 00:00:00 +0000 + + /entries/Boolos_Curious_Inference_Automated.html + + + + + Automation of Boolos' Curious Inference in Isabelle/HOL + /entries/Boolos_Curious_Inference_Automated.html + Mon, 05 Dec 2022 00:00:00 +0000 + + /entries/Boolos_Curious_Inference_Automated.html + + + + + A Verified Translation of Multitape Turing Machines into Singletape Turing Machines + /entries/Multitape_To_Singletape_TM.html + Wed, 30 Nov 2022 00:00:00 +0000 + + /entries/Multitape_To_Singletape_TM.html + + + + + Making Arbitrary Relational Calculus Queries Safe-Range + /entries/Safe_Range_RC.html + Wed, 28 Sep 2022 00:00:00 +0000 + + /entries/Safe_Range_RC.html + + + + + Stalnaker's Epistemic Logic + /entries/Stalnaker_Logic.html + Fri, 23 Sep 2022 00:00:00 +0000 + + /entries/Stalnaker_Logic.html + + + + + Soundness and Completeness of Implicational Logic + /entries/Implicational_Logic.html + Tue, 13 Sep 2022 00:00:00 +0000 + + /entries/Implicational_Logic.html + + + + + Soundness and Completeness of Implicational Logic + /entries/Implicational_Logic.html + Tue, 13 Sep 2022 00:00:00 +0000 + + /entries/Implicational_Logic.html + + + + + Boolos's Curious Inference in Isabelle/HOL + /entries/Boolos_Curious_Inference.html + Mon, 20 Jun 2022 00:00:00 +0000 + + /entries/Boolos_Curious_Inference.html + + + + + Diophantine Equations and the DPRM Theorem + /entries/DPRM_Theorem.html + Mon, 06 Jun 2022 00:00:00 +0000 + + /entries/DPRM_Theorem.html + + + + + Reducing Rewrite Properties to Properties on Ground Terms + /entries/Rewrite_Properties_Reduction.html + Thu, 02 Jun 2022 00:00:00 +0000 + + /entries/Rewrite_Properties_Reduction.html + + + + + The Generalized Multiset Ordering is NP-Complete + /entries/Multiset_Ordering_NPC.html + Wed, 20 Apr 2022 00:00:00 +0000 + + /entries/Multiset_Ordering_NPC.html + + + + + Ackermann's Function Is Not Primitive Recursive + /entries/Ackermanns_not_PR.html + Wed, 23 Mar 2022 00:00:00 +0000 + + /entries/Ackermanns_not_PR.html + + + + + A Naive Prover for First-Order Logic + /entries/FOL_Seq_Calc3.html + Tue, 22 Mar 2022 00:00:00 +0000 + + /entries/FOL_Seq_Calc3.html + + + + + A Naive Prover for First-Order Logic + /entries/FOL_Seq_Calc3.html + Tue, 22 Mar 2022 00:00:00 +0000 + + /entries/FOL_Seq_Calc3.html + + + + + A Naive Prover for First-Order Logic + /entries/FOL_Seq_Calc3.html + Tue, 22 Mar 2022 00:00:00 +0000 + + /entries/FOL_Seq_Calc3.html + + + + + The Independence of the Continuum Hypothesis in Isabelle/ZF + /entries/Independence_CH.html + Sun, 06 Mar 2022 00:00:00 +0000 + + /entries/Independence_CH.html + + + + + Transitive Models of Fragments of ZFC + /entries/Transitive_Models.html + Thu, 03 Mar 2022 00:00:00 +0000 + + /entries/Transitive_Models.html + + + + + Wetzel's Problem and the Continuum Hypothesis + /entries/Wetzels_Problem.html + Fri, 18 Feb 2022 00:00:00 +0000 + + /entries/Wetzels_Problem.html + + + + + First-Order Query Evaluation + /entries/Eval_FO.html + Tue, 15 Feb 2022 00:00:00 +0000 + + /entries/Eval_FO.html + + + + + First-Order Theory of Rewriting + /entries/FO_Theory_Rewriting.html + Wed, 02 Feb 2022 00:00:00 +0000 + + /entries/FO_Theory_Rewriting.html + + + + + First-Order Theory of Rewriting + /entries/FO_Theory_Rewriting.html + Wed, 02 Feb 2022 00:00:00 +0000 + + /entries/FO_Theory_Rewriting.html + + + + + A Sequent Calculus Prover for First-Order Logic with Functions + /entries/FOL_Seq_Calc2.html + Mon, 31 Jan 2022 00:00:00 +0000 + + /entries/FOL_Seq_Calc2.html + + + + + A Sequent Calculus Prover for First-Order Logic with Functions + /entries/FOL_Seq_Calc2.html + Mon, 31 Jan 2022 00:00:00 +0000 + + /entries/FOL_Seq_Calc2.html + + + + + A Sequent Calculus Prover for First-Order Logic with Functions + /entries/FOL_Seq_Calc2.html + Mon, 31 Jan 2022 00:00:00 +0000 + + /entries/FOL_Seq_Calc2.html + + + + + Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL + /entries/PAL.html + Mon, 08 Nov 2021 00:00:00 +0000 + + /entries/PAL.html + + + + + Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL + /entries/SimplifiedOntologicalArgument.html + Mon, 08 Nov 2021 00:00:00 +0000 + + /entries/SimplifiedOntologicalArgument.html + + + + + Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL + /entries/SimplifiedOntologicalArgument.html + Mon, 08 Nov 2021 00:00:00 +0000 + + /entries/SimplifiedOntologicalArgument.html + + + + + Belief Revision Theory + /entries/Belief_Revision.html + Tue, 19 Oct 2021 00:00:00 +0000 + + /entries/Belief_Revision.html + + + + + Soundness and Completeness of an Axiomatic System for First-Order Logic + /entries/FOL_Axiomatic.html + Fri, 24 Sep 2021 00:00:00 +0000 + + /entries/FOL_Axiomatic.html + + + + + Soundness and Completeness of an Axiomatic System for First-Order Logic + /entries/FOL_Axiomatic.html + Fri, 24 Sep 2021 00:00:00 +0000 + + /entries/FOL_Axiomatic.html + + + + + A Formalization of Weighted Path Orders and Recursive Path Orders + /entries/Weighted_Path_Order.html + Thu, 16 Sep 2021 00:00:00 +0000 + + /entries/Weighted_Path_Order.html + + + + + Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories + /entries/CZH_Foundations.html + Mon, 06 Sep 2021 00:00:00 +0000 + + /entries/CZH_Foundations.html + + + + + Public Announcement Logic + /entries/Public_Announcement_Logic.html + Thu, 17 Jun 2021 00:00:00 +0000 + + /entries/Public_Announcement_Logic.html + + + + + Isabelle's Metalogic: Formalization and Proof Checker + /entries/Metalogic_ProofChecker.html + Tue, 27 Apr 2021 00:00:00 +0000 + + /entries/Metalogic_ProofChecker.html + + + + + Mereology + /entries/Mereology.html + Mon, 01 Mar 2021 00:00:00 +0000 + + /entries/Mereology.html + + + + + Solution to the xkcd Blue Eyes puzzle + /entries/Blue_Eyes.html + Sat, 30 Jan 2021 00:00:00 +0000 + + /entries/Blue_Eyes.html + + + + + Cofinality and the Delta System Lemma + /entries/Delta_System_Lemma.html + Sun, 27 Dec 2020 00:00:00 +0000 + + /entries/Delta_System_Lemma.html + + + + + Topological semantics for paraconsistent and paracomplete logics + /entries/Topological_Semantics.html + Thu, 17 Dec 2020 00:00:00 +0000 + + /entries/Topological_Semantics.html + + + + + An Abstract Formalization of Gödel's Incompleteness Theorems + /entries/Goedel_Incompleteness.html + Wed, 16 Sep 2020 00:00:00 +0000 + + /entries/Goedel_Incompleteness.html + + + + + From Abstract to Concrete Gödel's Incompleteness Theorems—Part I + /entries/Goedel_HFSet_Semantic.html + Wed, 16 Sep 2020 00:00:00 +0000 + + /entries/Goedel_HFSet_Semantic.html + + + + + From Abstract to Concrete Gödel's Incompleteness Theorems—Part II + /entries/Goedel_HFSet_Semanticless.html + Wed, 16 Sep 2020 00:00:00 +0000 + + /entries/Goedel_HFSet_Semanticless.html + + + + + Robinson Arithmetic + /entries/Robinson_Arithmetic.html + Wed, 16 Sep 2020 00:00:00 +0000 + + /entries/Robinson_Arithmetic.html + + + + + Syntax-Independent Logic Infrastructure + /entries/Syntax_Independent_Logic.html + Wed, 16 Sep 2020 00:00:00 +0000 + + /entries/Syntax_Independent_Logic.html + + + + + Some classical results in inductive inference of recursive functions + /entries/Inductive_Inference.html + Mon, 31 Aug 2020 00:00:00 +0000 + + /entries/Inductive_Inference.html + + + + + Extensions to the Comprehensive Framework for Saturation Theorem Proving + /entries/Saturation_Framework_Extensions.html + Tue, 25 Aug 2020 00:00:00 +0000 + + /entries/Saturation_Framework_Extensions.html + + + + + Ordinal Partitions + /entries/Ordinal_Partitions.html + Mon, 03 Aug 2020 00:00:00 +0000 + + /entries/Ordinal_Partitions.html + + + + + A Formalization of Knuth–Bendix Orders + /entries/Knuth_Bendix_Order.html + Wed, 13 May 2020 00:00:00 +0000 + + /entries/Knuth_Bendix_Order.html + + + + + Recursion Theorem in ZF + /entries/Recursion-Addition.html + Mon, 11 May 2020 00:00:00 +0000 + + /entries/Recursion-Addition.html + + + + + An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation + /entries/LTL_Normal_Form.html + Fri, 08 May 2020 00:00:00 +0000 + + /entries/LTL_Normal_Form.html + + + + + Formalization of Forcing in Isabelle/ZF + /entries/Forcing.html + Wed, 06 May 2020 00:00:00 +0000 + + /entries/Forcing.html + + + + + A Comprehensive Framework for Saturation Theorem Proving + /entries/Saturation_Framework.html + Thu, 09 Apr 2020 00:00:00 +0000 + + /entries/Saturation_Framework.html + + + + + Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations + /entries/MFODL_Monitor_Optimized.html + Thu, 09 Apr 2020 00:00:00 +0000 + + /entries/MFODL_Monitor_Optimized.html + + + + + Implementing the Goodstein Function in λ-Calculus + /entries/Goodstein_Lambda.html + Fri, 21 Feb 2020 00:00:00 +0000 + + /entries/Goodstein_Lambda.html + + + + + Formalizing a Seligman-Style Tableau System for Hybrid Logic + /entries/Hybrid_Logic.html + Fri, 20 Dec 2019 00:00:00 +0000 + + /entries/Hybrid_Logic.html + + + + + Zermelo Fraenkel Set Theory in Higher-Order Logic + /entries/ZFC_in_HOL.html + Thu, 24 Oct 2019 00:00:00 +0000 + + /entries/ZFC_in_HOL.html + + + + + Aristotle's Assertoric Syllogistic + /entries/Aristotles_Assertoric_Syllogistic.html + Tue, 08 Oct 2019 00:00:00 +0000 + + /entries/Aristotles_Assertoric_Syllogistic.html + + + + + A Sequent Calculus for First-Order Logic + /entries/FOL_Seq_Calc1.html + Thu, 18 Jul 2019 00:00:00 +0000 + + /entries/FOL_Seq_Calc1.html + + + + + A Verified Code Generator from Isabelle/HOL to CakeML + /entries/CakeML_Codegen.html + Mon, 08 Jul 2019 00:00:00 +0000 + + /entries/CakeML_Codegen.html + + + + + Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic + /entries/MFOTL_Monitor.html + Thu, 04 Jul 2019 00:00:00 +0000 + + /entries/MFOTL_Monitor.html + + + + + A General Theory of Syntax with Bindings + /entries/Binding_Syntax_Theory.html + Sat, 06 Apr 2019 00:00:00 +0000 + + /entries/Binding_Syntax_Theory.html + + + + + Universal Turing Machine + /entries/Universal_Turing_Machine.html + Fri, 08 Feb 2019 00:00:00 +0000 + + /entries/Universal_Turing_Machine.html + + + + + A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover + /entries/Functional_Ordered_Resolution_Prover.html + Fri, 23 Nov 2018 00:00:00 +0000 + + /entries/Functional_Ordered_Resolution_Prover.html + + + + + Graph Saturation + /entries/Graph_Saturation.html + Fri, 23 Nov 2018 00:00:00 +0000 + + /entries/Graph_Saturation.html + + + + + Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL + /entries/GewirthPGCProof.html + Tue, 30 Oct 2018 00:00:00 +0000 + + /entries/GewirthPGCProof.html + + + + + Epistemic Logic: Completeness of Modal Logics + /entries/Epistemic_Logic.html + Mon, 29 Oct 2018 00:00:00 +0000 + + /entries/Epistemic_Logic.html + + + + + Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms + /entries/Lambda_Free_EPO.html + Fri, 19 Oct 2018 00:00:00 +0000 + + /entries/Lambda_Free_EPO.html + + + + + Minsky Machines + /entries/Minsky_Machines.html + Tue, 14 Aug 2018 00:00:00 +0000 + + /entries/Minsky_Machines.html + + + + + First-Order Terms + /entries/First_Order_Terms.html + Tue, 06 Feb 2018 00:00:00 +0000 + + /entries/First_Order_Terms.html + + + + + Formalization of Bachmair and Ganzinger's Ordered Resolution Prover + /entries/Ordered_Resolution_Prover.html + Thu, 18 Jan 2018 00:00:00 +0000 + + /entries/Ordered_Resolution_Prover.html + + + + + Hybrid Multi-Lane Spatial Logic + /entries/Hybrid_Multi_Lane_Spatial_Logic.html + Mon, 06 Nov 2017 00:00:00 +0000 + + /entries/Hybrid_Multi_Lane_Spatial_Logic.html + + + + + Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument + /entries/Lowe_Ontological_Argument.html + Thu, 21 Sep 2017 00:00:00 +0000 + + /entries/Lowe_Ontological_Argument.html + + + + + Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL + /entries/PLM.html + Sun, 17 Sep 2017 00:00:00 +0000 + + /entries/PLM.html + + + + + Anselm's God in Isabelle/HOL + /entries/AnselmGod.html + Wed, 06 Sep 2017 00:00:00 +0000 + + /entries/AnselmGod.html + + + + + Propositional Proof Systems + /entries/Propositional_Proof_Systems.html + Wed, 21 Jun 2017 00:00:00 +0000 + + /entries/Propositional_Proof_Systems.html + + + + + Monad normalisation + /entries/Monad_Normalisation.html + Fri, 05 May 2017 00:00:00 +0000 + + /entries/Monad_Normalisation.html + + + + + Types, Tableaus and Gödel’s God in Isabelle/HOL + /entries/Types_Tableaus_and_Goedels_God.html + Mon, 01 May 2017 00:00:00 +0000 + + /entries/Types_Tableaus_and_Goedels_God.html + + + + + Differential Dynamic Logic + /entries/Differential_Dynamic_Logic.html + Mon, 13 Feb 2017 00:00:00 +0000 + + /entries/Differential_Dynamic_Logic.html + + + + + Abstract Soundness + /entries/Abstract_Soundness.html + Fri, 10 Feb 2017 00:00:00 +0000 + + /entries/Abstract_Soundness.html + + + + + First-Order Logic According to Harrison + /entries/FOL_Harrison.html + Sun, 01 Jan 2017 00:00:00 +0000 + + /entries/FOL_Harrison.html + + + + + Paraconsistency + /entries/Paraconsistency.html + Wed, 07 Dec 2016 00:00:00 +0000 + + /entries/Paraconsistency.html + + + + + Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms + /entries/Lambda_Free_KBOs.html + Sat, 12 Nov 2016 00:00:00 +0000 + + /entries/Lambda_Free_KBOs.html + + + + + Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals + /entries/Nested_Multisets_Ordinals.html + Sat, 12 Nov 2016 00:00:00 +0000 + + /entries/Nested_Multisets_Ordinals.html + + + + + Modal Logics for Nominal Transition Systems + /entries/Modal_Logics_for_NTS.html + Tue, 25 Oct 2016 00:00:00 +0000 + + /entries/Modal_Logics_for_NTS.html + + + + + Allen's Interval Calculus + /entries/Allen_Calculus.html + Thu, 29 Sep 2016 00:00:00 +0000 + + /entries/Allen_Calculus.html + + + + + Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms + /entries/Lambda_Free_RPOs.html + Fri, 23 Sep 2016 00:00:00 +0000 + + /entries/Lambda_Free_RPOs.html + + + + + A Variant of the Superposition Calculus + /entries/SuperCalc.html + Tue, 06 Sep 2016 00:00:00 +0000 + + /entries/SuperCalc.html + + + + + Surprise Paradox + /entries/Surprise_Paradox.html + Sun, 17 Jul 2016 00:00:00 +0000 + + /entries/Surprise_Paradox.html + + + + + The Resolution Calculus for First-Order Logic + /entries/Resolution_FOL.html + Thu, 30 Jun 2016 00:00:00 +0000 + + /entries/Resolution_FOL.html + + + + + The Z Property + /entries/Rewriting_Z.html + Thu, 30 Jun 2016 00:00:00 +0000 + + /entries/Rewriting_Z.html + + + + + The meta theory of the Incredible Proof Machine + /entries/Incredible_Proof_Machine.html + Fri, 20 May 2016 00:00:00 +0000 + + /entries/Incredible_Proof_Machine.html + + + + + Propositional Resolution and Prime Implicates Generation + /entries/PropResPI.html + Fri, 11 Mar 2016 00:00:00 +0000 + + /entries/PropResPI.html + + + + + Linear Temporal Logic + /entries/LTL.html + Tue, 01 Mar 2016 00:00:00 +0000 + + /entries/LTL.html + + + + + Decreasing Diagrams II + /entries/Decreasing-Diagrams-II.html + Thu, 20 Aug 2015 00:00:00 +0000 + + /entries/Decreasing-Diagrams-II.html + + + + + Derivatives of Logical Formulas + /entries/Formula_Derivatives.html + Thu, 28 May 2015 00:00:00 +0000 + + /entries/Formula_Derivatives.html + + + + + Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions + /entries/MSO_Regex_Equivalence.html + Thu, 12 Jun 2014 00:00:00 +0000 + + /entries/MSO_Regex_Equivalence.html + + + + + Boolean Expression Checkers + /entries/Boolean_Expression_Checkers.html + Sun, 08 Jun 2014 00:00:00 +0000 + + /entries/Boolean_Expression_Checkers.html + + + + + A shallow embedding of HyperCTL* + /entries/HyperCTL.html + Wed, 16 Apr 2014 00:00:00 +0000 + + /entries/HyperCTL.html + + + + + Abstract Completeness + /entries/Abstract_Completeness.html + Wed, 16 Apr 2014 00:00:00 +0000 + + /entries/Abstract_Completeness.html + + + + + Gödel's Incompleteness Theorems + /entries/Incompleteness.html + Sun, 17 Nov 2013 00:00:00 +0000 + + /entries/Incompleteness.html + + + + + The Hereditarily Finite Sets + /entries/HereditarilyFinite.html + Sun, 17 Nov 2013 00:00:00 +0000 + + /entries/HereditarilyFinite.html + + + + + Gödel's God in Isabelle/HOL + /entries/GoedelGod.html + Tue, 12 Nov 2013 00:00:00 +0000 + + /entries/GoedelGod.html + + + + + Decreasing Diagrams + /entries/Decreasing-Diagrams.html + Fri, 01 Nov 2013 00:00:00 +0000 + + /entries/Decreasing-Diagrams.html + + + + + Sound and Complete Sort Encodings for First-Order Logic + /entries/Sort_Encodings.html + Thu, 27 Jun 2013 00:00:00 +0000 + + /entries/Sort_Encodings.html + + + + + Interval Temporal Logic on Natural Numbers + /entries/Nat-Interval-Logic.html + Wed, 23 Feb 2011 00:00:00 +0000 + + /entries/Nat-Interval-Logic.html + + + + + Abstract Rewriting + /entries/Abstract-Rewriting.html + Mon, 14 Jun 2010 00:00:00 +0000 + + /entries/Abstract-Rewriting.html + + + + + Free Boolean Algebra + /entries/Free-Boolean-Algebra.html + Mon, 29 Mar 2010 00:00:00 +0000 + + /entries/Free-Boolean-Algebra.html + + + + + Formalizing the Logic-Automaton Connection + /entries/Presburger-Automata.html + Thu, 03 Dec 2009 00:00:00 +0000 + + /entries/Presburger-Automata.html + + + + + Ordinals and Cardinals + /entries/Ordinals_and_Cardinals.html + Tue, 01 Sep 2009 00:00:00 +0000 + + /entries/Ordinals_and_Cardinals.html + + + + + Invertibility in Sequent Calculi + /entries/SequentInvertibility.html + Fri, 28 Aug 2009 00:00:00 +0000 + + /entries/SequentInvertibility.html + + + + + Recursion Theory I + /entries/Recursion-Theory-I.html + Sat, 05 Apr 2008 00:00:00 +0000 + + /entries/Recursion-Theory-I.html + + + + + Quantifier Elimination for Linear Arithmetic + /entries/LinearQuantifierElim.html + Fri, 11 Jan 2008 00:00:00 +0000 + + /entries/LinearQuantifierElim.html + + + + + First-Order Logic According to Fitting + /entries/FOL-Fitting.html + Thu, 02 Aug 2007 00:00:00 +0000 + + /entries/FOL-Fitting.html + + + + + Countable Ordinals + /entries/Ordinal.html + Fri, 11 Nov 2005 00:00:00 +0000 + + /entries/Ordinal.html + + + + + A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic + /entries/Verified-Prover.html + Tue, 28 Sep 2004 00:00:00 +0000 + + /entries/Verified-Prover.html + + + + + Completeness theorem + /entries/Completeness.html + Mon, 20 Sep 2004 00:00:00 +0000 + + /entries/Completeness.html + + + + +