[{"_1":2,"_161":-5,"_162":-5},"loaderData",{"_3":4,"_17":18,"_25":26,"_140":141},"root",{"_5":-5,"_6":-7,"_7":8,"_9":-7,"_10":11,"_12":-7,"_13":14,"_15":16},"currentUser","primaryEmail","siteVerification","6LeIxAcTAAAAAJcZVRqyHh71UMIEGNQ_MXjiZKhI","toast","enableDev",false,"incidentStatus","theme","system","contrast","normal","routes/_layout",{"_19":-5,"_20":21,"_22":21,"_23":11,"_24":21},"username","isAskGordonEnabled",true,"isUsingNewTemplate","showMinimalLanding","showHoneypotTrap","routes/_layout.r.$namespace.$reponame",{"_27":28,"_29":-5,"_30":11,"_31":11,"_32":33,"_34":35,"_36":-5,"_37":11,"_38":39,"_88":-5,"_89":90,"_129":-5,"_130":11,"_131":21,"_132":11,"_133":-5,"_134":11,"_135":-5,"_136":137,"_138":91,"_139":-7},"canonicalUrl","https://hub.docker.com/r/lionell/math-logic/tags","mcpServer","canSeeDockerfile","canSeeAutobuilds","namespace","lionell","reponame","math-logic","cloudBuildSource","isAutobuildsAvailable","repo",{"_40":41,"_42":43,"_45":46,"_47":48,"_49":11,"_50":51,"_52":53,"_54":55,"_57":35,"_32":33,"_58":59,"_60":44,"_61":62,"_63":64,"_65":66,"_67":-5,"_68":62,"_69":70,"_71":11,"_72":33,"_73":74,"_79":11,"_80":81,"_85":33,"_86":87},"categories",[],"content_types",[44],"image","date_registered","2018-06-17T12:43:09.018753Z","description","Implementation of sequential method for classic first-order-logic","is_private","last_updated","2019-03-07T20:54:03.676002Z","last_modified","2024-10-16T13:48:34.145251Z","media_types",[56],"application/vnd.docker.container.image.v1+json","name","pull_count",185,"repository_type","star_count",0,"status",1,"status_description","active","source","collaborator_count","full_description","# Sequential method\n\n

\n $\"Logo\"$ \n

\n\nA prover of logical formulas. Core of application is Sequential Method algorithm.\n\n## How it works\nApplication is divided in several independent modules:\n 1. [Parser][1-1] parse input string into AST.\n 1. [Tokenizer][1-1-1] split input expression into lexemes.\n 2. [Infix-to-Postfix converter][1-1-2] converts infix list of lexemes\n to RPN(Reverse Polish Notation).\n 3. [Abstract Syntax Tree generator][1-1-3] converts list of\n tokens(token = lexeme + additional information) to tree.\n 2. [Sequential method][1-2] logic of application.\n 3. [Wrapper][1-3] wrap results of Sequential method to unique data structure for\n mapping to JSON.\n\n[1-1]: /src/main/java/io/github/lionell/utils/analysis/Parser.java\n[1-1-1]: /src/main/java/io/github/lionell/utils/analysis/Tokenizer.java\n[1-1-2]: /src/main/java/io/github/lionell/utils/analysis/InfixToPostfixConverter.java\n[1-1-3]: /src/main/java/io/github/lionell/utils/analysis/FormulaGenerator.java\n[1-2]: /src/main/java/io/github/lionell/utils/SequentialMethod.java\n[1-3]: /src/main/java/io/github/lionell/utils/WrapBuilder.java\n\nNow let's move to the **heart** of application.\n\n### Algorithm\nHere are description of one algorithm iteration.\n 1. If all leaves are closed, **finish with positive verdict**.\n 2. If all leaves are atomic, **finish with negative verdict**.\n 3. For each non-atomic, non-closed leaf\n * Expand leaf.\n * Simplify result leaves.\n 4. Goto step 1\n\nThere is situation when algorithm will go to **INFINITE LOOP**.\nIn this case we can use [König's infinity lemma][kenigs] to\n**finish with negative result**.\n\n[kenigs]: https://en.wikipedia.org/wiki/K%C3%B6nig%27s_lemma\n\n#### Sequential formulas\n\n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n

mark	notation	branches
₊!	₊!A, Σ	_-A, Σ
_-!	_-!A, Σ	₊A, Σ
₊v	₊(A v B), Σ	₊A, Σ	₊B, Σ
_-v	_-(A v B), Σ	_-A, _-B, Σ
₊&	₊(A & B), Σ	₊A, ₊B, Σ
_-&	_-(A & B), Σ	_-A, Σ	_-B, Σ
₊->	₊(A -> B), Σ	_-A, Σ	₊B, Σ
_-->	_-(A -> B), Σ	₊A, _-B, Σ
₊∃	₊∃xA, Σ	₊A_x[y], Σ
_-∃	_-∃xA, Σ	\n _-A_x[z₁],\n ...,\n _-A_x[z_m],\n Σ,\n _-∃xA\n
₊∀	₊∀xA, Σ	\n ₊A_x[z₁],\n ...,\n ₊A_x[z_m],\n Σ,\n ₊∀xA\n
_-∀	_-∀xA, Σ	_-A_x[y], Σ

\n\nWhere\n * y denotes **new unique** name.\n * z₁, ..., z_m denotes names **used in current sequence**.\n * A_x[y] denotes **renomination** of predicate from x to y.\n\n### Let's look at examples\n#### Example 1\nFirst example demonstrates how exactly sequences is expanding when implication\nand disjunction are in charge.\n```\n P[x] = P[x] | Q[x]\n |\n v\n-(P[x] -> P[x] | Q[x])\n |\n v\n+P[x], -(P[x] | Q[x])\n |\n v\n -P[x], -Q[x], +P[x]\n |\n v\n X\n```\nAs you can see sequential tree has only one branch, and it's closed.\nAccording to algorithm above, expression is **truthful**.\nIt's quite simple example, so let's move to something more interesting.\n\n#### Example 2\nHere is more complicated example with quantifiers.\nIt's also truthful, but now we have two different closed branches.\n```\n #xP[x] -> Q[x] = P[x] -> #xQ[x]\n |\n v\n -((#xP[x] -> Q[x]) -> P[x] -> #xQ[x])\n |\n v\n +(#xP[x] -> Q[x]), -(P[x] -> #xQ[x])\n / \\\n / \\\n v v\n -#xP[x], -(P[x] -> #xQ[x]) +Q[x], -(P[x] -> #xQ[x])\n | |\n v v\n-P[x], -(P[x] -> #xQ[x]), -#xP[x] +P[x], -#xQ[x], +Q[x]\n | |\n v v\n +P[x], -#xQ[x], -P[x], -#xP[x] -Q[x], +P[x], +Q[x], -#xQ[x]\n | |\n v v\n X X\n```\nAs you can see all two branches closed at the same time. So expression is\ntruthful and no counter examples exists.\n\n#### Example 3\nThis example show you how to deal with unclosed sequences, and how to get a\ncounter example.\n```\n P[x] -> #xQ[x] = #xP[x] -> Q[x]\n |\n v\n -(P[x] -> #xQ[x] -> #xP[x] -> Q[x])\n |\n v\n +(P[x] -> #xQ[x]), -(#xP[x] -> Q[x])\n / \\\n / \\\n v v\n-P[x], -(#xP[x] -> Q[x]) +#xQ[x], -(#xP[x] -> Q[x])\n | |\n v v\n +#xP[x], -Q[x], -P[x] +Q[z], -(#xP[x] -> Q[x])\n | |\n v v\n +P[y], -Q[x], -P[x] +#xP[x], -Q[x], +Q[z]\n |\n v\n +P[w], -Q[x], +Q[z]\n```\n\n##### Left branch\n\n| name | delta | values |\n|:----:|:--------|:---------------------|\n| | x -> a, | P\\[a\\] := **False,** |\n| A | y -> b | P\\[b\\] := **True,** |\n| | | Q\\[a\\] := **False** |\n\nLet's try to build interpretation on this counter example. There are many\ndifferent options, but we can stop on:\n```\nx := integer\nP[x] := x == 1\nQ[x] := x != x // always false\n```\n\n##### Right branch\n\n| name | delta | values |\n|:----:|:--------|:--------------------|\n| | x -> a, | Q\\[a] := **False,** |\n| B | z -> b, | Q\\[b] := **True,** |\n| | w -> c | P\\[c] := **True** |\n\nIn this case we can use next interpretation:\n```\nx := integer\nP[x] := (x + x) % 2 == 0 // always true\nQ[x] := x % 2 == 1\n```\n\n##### Summary\nWe have got two unclosed branches. Each one produces unique counter example.\nEach counter example can give us many different interpretations. We have\nalready built some of them. You can manually check these interpretations,\nto ensure that expression is false. Just evaluate input expression with these\ninterpretations.\n\nLet's stop at this example and move forward to syntax overview.\n\n## Language specification\nThis is language grammar in [Backus-Naur-Form][bnf].\n\n[bnf]: https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form\n\n```HTML+PHP\n ::= \"=\" \n ::= [ \"(\" ]\n \n | \n | \n [ \")\" ]\n ::= \"[\" \"]\"\n ::= { }\n ::= { \",\" }\n ::= { }\n\n ::= \n | \n ::=

\n ::= \"&\"\n | \"|\"\n | \"->\"\n ::= \"!\" \n\n ::=

\n ::= \"#\" Stands for \"exists\"\n | \"@\" Stands for \"for all\"\n\n ::= \"a\"\n | \"b\"\n | ...\n | \"z\"\n ::= \"A\"\n | \"B\"\n | ...\n | \"Z\"\n```\n\nIf your expression **does not fit** this grammar then application will rise an\nparser exception and inform you with `error` field of response.\n\n### Valid expressions\nSome valid examples of expressions:\n * `P[x] = Q[x]`\n * `P[x] = P[x] | Q[x]`\n * `#xP[x] -> Q[x] = P[x] -> #xQ[x]`\n * `#x@yP[x, y] = @y#xP[x, y]`\n * `P[x] -> #xQ[x] = #xP[x] -> Q[x]`\n * `P[x] | Q[x] | R[x] | T[x] | S[x] = @xP[x]`\n * `@xP[x] = Q[x]`\n\n## API\nThere are only one service available, named `check`. To use it your query\nshould contains field named `expr` with expression you want to check.\nBoth `get` and `post` methods are supported.\n\n### API Usage\nSimple request `check?expr=P[x]=P[x]|Q[x]` will give you response\nlisted below.\n\n```JSON\n{\n \"tree\":{\n \"root\":{\n \"formulas\":[\n {\n \"formula\":\"P[x] -> Q[x]\",\n \"value\":false\n }\n ],\n \"children\":[\n {\n \"formulas\":[\n {\n \"formula\":\"P[x]\",\n \"value\":true\n },\n {\n \"formula\":\"Q[x]\",\n \"value\":false\n }\n ],\n \"children\":[],\n \"closed\":false\n }\n ],\n \"closed\":false\n }\n },\n \"verity\":false,\n \"examples\":[\n {\n \"name\":\"E\",\n \"delta\":{\n \"x\":\"m\"\n },\n \"example\":{\n \"P\":{\n \"[m]\":true\n },\n \"Q\":{\n \"[m]\":false\n }\n }\n }\n ],\n \"error\":null\n}\n```\n\nNow let's look closer to response structure.\n\n### Response structure\n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n

	name	type	description
response	tree	{root: node}	sequential tree with root node
verity	Boolean	null, if infinite loop
examples	[example]	list of examples
error	string	error message from server
node	formulas	[formula]	list of formulas
children	[node]	list of child nodes
closed	boolean	is sequence closed
formula	formula	string	actual formula
value	boolean	logical value
example	name	string	name of example
delta	{x -> a}	map of new variable names
example	{P[x] -> val}	map of predicates/variables/values

\n\n## Installation\n### Requirements\n * Java Runtime Environment with Java SE8 support\n * Maven 3 to build\n\n### Building\nYou can build app using Maven with ease. Just type `mvn clean package`.\nThis will generate JAR file `target/sequential-method-1.0-SNAPSHOT.jar`.\n\n### Running\nIf you are using Maven, you can run application without building using\n`mvn spring-boot:run`.\n\nOr if you have pre-built JAR you can run it by typing:\n\n`java -jar target/sequential-method-1.0-SNAPSHOT.jar`\n\n### Docker\nYou can run this application using prebuild docker image like this `docker run -it -p 8080:8080 lionell/math-logic`.\nAlternatively you can use Docker Compose `docker-compose up -d`. This will start service locally and expose port 8080.\n\n## Used materials\nHere is a list of materials used in app:\n * [D3.js](http://d3js.org) visualizing sequential tree\n * [HTML5 UP](http://html5up.net) design of main page\n * [Spring](https://spring.io) framework\n * [Maven](https://maven.apache.org) app architecture\n * [Docker](https://www.docker.com) isolated environment\n\n## Contributions\nHere I want to say thanks to my friend [Fetiorin](http://vk.com/id234442497)\nwho helped me with this app.\n\nHe did a great job on the client-side.\n\n## Licence\nMIT\n","has_starred","hub_user","immutable_tags_settings",{"_75":11,"_76":77},"enabled","rules",[78],".*","is_automated","permissions",{"_82":21,"_83":11,"_84":11},"read","write","admin","user","storage_size",855770108,"orgData","recentTags",[91],{"_92":44,"_93":94,"_95":96,"_97":98,"_99":100,"_50":118,"_119":94,"_120":33,"_121":56,"_57":122,"_123":124,"_125":109,"_126":118,"_127":66,"_128":21},"content_type","creator",1244536,"full_size",497418197,"id",29341690,"images",[101],{"_102":103,"_104":105,"_106":107,"_108":109,"_110":111,"_112":113,"_114":107,"_115":-5,"_116":96,"_63":66,"_117":-5},"architecture","amd64","digest","sha256:d44f3423050469e39030f7535036300d50afec206e1e2bd9ec9ce07d0f46af89","features","","last_pulled","2026-09-29T18:39:07.285035284Z","last_pushed","2019-03-07T20:54:04Z","os","linux","os_features","os_version","size","variant","2019-03-07T20:54:03.371836Z","last_updater","last_updater_username","media_type","latest","repository",5629711,"tag_last_pulled","tag_last_pushed","tag_status","v2","sbxKitMetadata","isPotentialSpam","isHubSbxKitsEnabled","showSbxLogoOverride","sbxTrademarkText","displaySecurityMetadata","tagAttestations","tagsHaveAttestations",[],"selectedTag","attestationsUrl","routes/_layout.r.$namespace.$reponame.tags",{"_38":142,"_149":150,"_136":159,"_160":11},{"_40":143,"_42":144,"_45":46,"_47":48,"_49":11,"_50":51,"_52":53,"_54":145,"_57":35,"_32":33,"_58":59,"_60":44,"_61":62,"_63":64,"_65":66,"_67":-5,"_68":62,"_69":70,"_71":11,"_72":33,"_73":146,"_79":11,"_80":148,"_85":33,"_86":87},[],[44],[56],{"_75":11,"_76":147},[78],{"_82":21,"_83":11,"_84":11},"tags",{"_151":64,"_152":-5,"_153":-5,"_154":155},"count","next","previous","results",[156],{"_92":44,"_93":94,"_95":96,"_97":98,"_99":157,"_50":118,"_119":94,"_120":33,"_121":56,"_57":122,"_123":124,"_125":109,"_126":118,"_127":66,"_128":21},[158],{"_102":103,"_104":105,"_106":107,"_108":109,"_110":111,"_112":113,"_114":107,"_115":-5,"_116":96,"_63":66,"_117":-5},[],"canDeleteTags","actionData","errors"]

lionell/math-logic

Tags for lionell/math-logic